Class ContensionSatInconsistencyMeasure

  • All Implemented Interfaces:
    PostulateEvaluatable<PlFormula>, InconsistencyMeasure<BeliefSet<PlFormula,​?>>

    public class ContensionSatInconsistencyMeasure
    extends SatBasedInconsistencyMeasure
    This class implements a SAT encoding of the contension inconsistency measure, originally proposed in [Grant, Hunter. "Measuring consistency gain and information loss in step-wise inconsistency resolution", ECSQARU'11].
    This measure is defined on paraconsistent models (three-valued models with truth values F,T,B) of a knowledge base by taking the minimal number of B-valued propositions needed in a model of the knowledge base.
    Author:
    Anna Gessler
    • Constructor Detail

      • ContensionSatInconsistencyMeasure

        public ContensionSatInconsistencyMeasure​(SatSolver solver)
        Create a new ContensionSatInconsistencyMeasure with the given SAT solver.
        Parameters:
        solver - some SAT solver
      • ContensionSatInconsistencyMeasure

        public ContensionSatInconsistencyMeasure()
        Create a new ContensionSatInconsistencyMeasure with the default SAT solver.
    • Method Detail

      • getSATEncoding

        public PlBeliefSet getSATEncoding​(java.util.Collection<PlFormula> kb,
                                          int upper_bound)
      • toString

        public java.lang.String toString()
        Overrides:
        toString in class java.lang.Object