Class AbstractSatExtensionReasoner

    • Constructor Detail

      • AbstractSatExtensionReasoner

        public AbstractSatExtensionReasoner​(SatSolver solver)
        Instantiates a new reasoner that uses the given SAT solver
        Parameters:
        solver - some AT solver
    • Method Detail

      • getPropositionalCharacterisation

        public PlBeliefSet getPropositionalCharacterisation​(DungTheory aaf)
        Creates a propositional representation of the set of labelings of the given Dung theory that are consistent with the given semantics. This means that for every argument A in the theory three propositions are created: in_A, out_A, undec_A. For every attack A->B the formula "in_A => out_B" is added to the belief set. Depending on the actual semantics further propositional formulas are added. For example, for any admissable semantics and unattacked argument A, the constraint "\top=>in_A" is added; another constraint added for admissable semantics is, given any argument A and attackers B1...BN, add the constraint in_A => out_B1 ^ ... ^ out_BN.
        Parameters:
        aaf - a Dung Thery
        Returns:
        a propositional belief set.