Class LeviMultipleBaseRevisionOperator<T extends ClassicalFormula>

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

    public class LeviMultipleBaseRevisionOperator<T extends ClassicalFormula>
    extends MultipleBaseRevisionOperator<T>
    This class implements the Levi identity for multiple revision, ie. an revision that is composed of the contraction with the negated set of formulas and then expansion with those formulas.
    Author:
    Matthias Thimm
    • Method Summary

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

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

      • LeviMultipleBaseRevisionOperator

        public LeviMultipleBaseRevisionOperator​(MultipleBaseContractionOperator<T> contraction,
                                                MultipleBaseExpansionOperator<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,
                                              java.util.Collection<T> formulas)
        Description copied from class: MultipleBaseRevisionOperator
        Revises the first collection of formulas by the second collection of formulas.
        Specified by:
        revise in class MultipleBaseRevisionOperator<T extends ClassicalFormula>
        Parameters:
        base - some collection of formulas.
        formulas - some formulas.
        Returns:
        the revised collection.