Class LeviBaseRevisionOperator<T extends ClassicalFormula>

  • Type Parameters:
    T - the type of formulas this operators works on.
    All Implemented Interfaces:
    BaseRevisionOperator<T>

    public class LeviBaseRevisionOperator<T extends ClassicalFormula>
    extends java.lang.Object
    implements BaseRevisionOperator<T>
    This class implements the Levi identity for revision, ie. an revision that is composed of the contraction with the negated formula and then expansion of the formula.
    Author:
    Matthias Thimm
    • Method Summary

      Modifier and Type Method Description
      java.util.Collection<T> revise​(java.util.Collection<T> base, T formula)
      Revises the given collection of formulas by the given formula.
      • Methods inherited from class java.lang.Object

        equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
    • Constructor Detail

      • LeviBaseRevisionOperator

        public LeviBaseRevisionOperator​(BaseContractionOperator<T> contraction,
                                        BaseExpansionOperator<T> expansion)
        Creates a new Levi base revision with the given contraction and expansion operators.
        Parameters:
        contraction - some contraction operator.
        expansion - some expansion operator.
    • Method Detail

      • revise

        public java.util.Collection<T> revise​(java.util.Collection<T> base,
                                              T formula)
        Description copied from interface: BaseRevisionOperator
        Revises the given collection of formulas by the given formula.
        Specified by:
        revise in interface BaseRevisionOperator<T extends ClassicalFormula>
        Parameters:
        base - some collection of formulas.
        formula - a formula
        Returns:
        the revised collection.