Uses of Class
org.tweetyproject.logics.pl.syntax.PlFormula
Package
Description
-
Uses of PlFormula in org.tweetyproject.action.query.syntax
Modifier and TypeClassDescriptionclass
This class represents an always query in the action query language S.class
This class represents a holds query in the action query language S.class
This class represents a necessarily query in the action query language S.class
Action queries are represented as propositional formulas with three possible types of propositions: "holds", "always" and "necessarily" propositions.ModifierConstructorDescriptionSActionQuery
(PlFormula formula) Creates a new action query with the given propositional formula and no grounding requirements.SActionQuery
(PlFormula formula, Set<GroundingRequirement> requirements) Creates a new action query with the given propositional formula and grounding requirements. -
Uses of PlFormula in org.tweetyproject.agents.dialogues
ModifierConstructorDescriptionExecutableFormulaSet
(Collection<? extends PlFormula> formulas) Creates a new set for the given formulas. -
Uses of PlFormula in org.tweetyproject.agents.dialogues.oppmodels
Modifier and TypeMethodDescriptionDeductiveEnvironment.getDialogueTrace()
Returns the current dialogue trace.DeductiveEnvironment.getDialogueTrace()
Returns the current dialogue trace. -
Uses of PlFormula in org.tweetyproject.arg.aspic.ruleformulagenerator
Modifier and TypeMethodDescriptionPlFormulaGenerator.getRuleFormula
(DefeasibleInferenceRule<PlFormula> r) Modifier and TypeMethodDescriptionPlFormulaGenerator.getRuleFormula
(DefeasibleInferenceRule<PlFormula> r) -
Uses of PlFormula in org.tweetyproject.arg.aspic.util
Modifier and TypeMethodDescriptionRandomAspicArgumentationTheoryGenerator.next()
Returns an ASPIC argumentation theory -
Uses of PlFormula in org.tweetyproject.arg.deductive.reasoner
Modifier and TypeMethodDescriptionAbstractDeductiveArgumentationReasoner.query
(DeductiveKnowledgeBase kb, PlFormula f) -
Uses of PlFormula in org.tweetyproject.arg.deductive.semantics
Modifier and TypeMethodDescriptionDeductiveArgument.getClaim()
Returns the claim of this argument.Modifier and TypeMethodDescriptionCollection<? extends PlFormula>
DeductiveArgument.getSupport()
Returns the support of this argument.ModifierConstructorDescriptionDeductiveArgument
(Collection<? extends PlFormula> support, PlFormula claim) Creates a new deductive argument with the given support and claim.DeductiveArgumentNode
(Collection<? extends PlFormula> support, PlFormula claim) Creates a new deductive argument node with the given support and claim (a unique ID is generated)ModifierConstructorDescriptionCompilationNode
(Collection<? extends PlFormula> formulas) Creates a new compilation node with the given set of formulas.DeductiveArgument
(Collection<? extends PlFormula> support, PlFormula claim) Creates a new deductive argument with the given support and claim.DeductiveArgumentNode
(Collection<? extends PlFormula> support, PlFormula claim) Creates a new deductive argument node with the given support and claim (a unique ID is generated) -
Uses of PlFormula in org.tweetyproject.arg.deductive.syntax
Modifier and TypeMethodDescriptionvoid
SimplePlRule.addPremise
(PlFormula arg0) DeductiveKnowledgeBase.getDeductiveArguments
(PlFormula claim) Computes all deductive arguments for the given claim.void
SimplePlRule.setConclusion
(PlFormula arg0) Modifier and TypeMethodDescriptionvoid
SimplePlRule.addPremises
(Collection<? extends PlFormula> arg0) ModifierConstructorDescriptionSimplePlLogicArgument
(Collection<SimplePlRule> _support, PlFormula _claim) SimplePlRule
(PlFormula _claim) SimplePlRule
(PlFormula _claim, Set<PlFormula> _support) ModifierConstructorDescriptionDeductiveKnowledgeBase
(Collection<? extends PlFormula> formulas) Creates a new knowledge base with the given set of formulas.SimplePlRule
(PlFormula _claim, Set<PlFormula> _support) -
Uses of PlFormula in org.tweetyproject.beliefdynamics.mas
ModifierConstructorDescriptionAbstractCredibilityComparer
(Collection<InformationObject<PlFormula>> formulas, Order<Agent> credOrder) Creates a new credibility comparer that is guided by the giving information which agents uttered the formulas and the credibility order.CredibilityCategorizer
(Collection<InformationObject<PlFormula>> formulas, Order<Agent> credOrder) Creates a new credibility categorizer that is guided by the giving information which agents uttered the formulas and the credibility order. -
Uses of PlFormula in org.tweetyproject.beliefdynamics.operators
Modifier and TypeMethodDescriptionArgumentativeRevisionOperator.revise
(Collection<PlFormula> base, Collection<PlFormula> formulas) CrMasArgumentativeRevisionOperator.revise
(Collection<InformationObject<PlFormula>> base, Collection<InformationObject<PlFormula>> formulas) CrMasSimpleRevisionOperator.revise
(Collection<InformationObject<PlFormula>> base, Collection<InformationObject<PlFormula>> formulas) Modifier and TypeMethodDescriptionArgumentativeRevisionOperator.revise
(Collection<PlFormula> base, Collection<PlFormula> formulas) CrMasArgumentativeRevisionOperator.revise
(Collection<InformationObject<PlFormula>> base, Collection<InformationObject<PlFormula>> formulas) CrMasSimpleRevisionOperator.revise
(Collection<InformationObject<PlFormula>> base, Collection<InformationObject<PlFormula>> formulas) -
Uses of PlFormula in org.tweetyproject.beliefdynamics.selectiverevision.argumentative
Modifier and TypeMethodDescriptionArgumentativeTransformationFunction.transform
(Collection<PlFormula> formulas) Modifier and TypeMethodDescriptionArgumentativeTransformationFunction.transform
(Collection<PlFormula> formulas) -
Uses of PlFormula in org.tweetyproject.logics.cl.reasoner
Modifier and TypeMethodDescriptionAbstractConditionalLogicReasoner.query
(ClBeliefSet beliefbase, PlFormula formula) -
Uses of PlFormula in org.tweetyproject.logics.cl.semantics
Modifier and TypeMethodDescriptionGets the rank of the given formula.Modifier and TypeMethodDescriptionvoid
RankingFunction.forceStrictness
(Set<PlFormula> formulas) Sets the rank of every interpretation i that does not satisfy the given set of formulas to RankingFunction.INFINITY. -
Uses of PlFormula in org.tweetyproject.logics.cl.syntax
Modifier and TypeMethodDescriptionvoid
Conditional.addPremise
(PlFormula premise) void
Conditional.setConclusion
(PlFormula conclusion) Modifier and TypeMethodDescriptionvoid
Conditional.addPremises
(Collection<? extends PlFormula> premises) ModifierConstructorDescriptionConditional
(PlFormula conclusion) Creates a new conditional with a tautological premise and given conclusion.Conditional
(PlFormula premise, PlFormula conclusion) Creates a new conditional with the given premise and conclusion. -
Uses of PlFormula in org.tweetyproject.logics.pcl.reasoner
Modifier and TypeMethodDescriptionabstract Double
AbstractPclReasoner.query
(PclBeliefSet beliefbase, PlFormula formula) DefaultMeReasoner.query
(PclBeliefSet beliefbase, PlFormula formula) GeneralizedMeReasoner.query
(PclBeliefSet beliefbase, PlFormula formula) -
Uses of PlFormula in org.tweetyproject.logics.pcl.semantics
Modifier and TypeClassDescriptionclass
ProbabilityDistribution<T extends Interpretation<PlBeliefSet,
PlFormula>> This class represents a probability distribution on some logical languageModifier and TypeMethodDescriptionstatic <S extends Interpretation<PlBeliefSet,
PlFormula>>
ProbabilityDistribution<S>ProbabilityDistribution.convexCombination
(double[] factors, ProbabilityDistribution<S>[] creators) Computes the convex combination of the given probability distributions P1,...,PN with parameters factors, i.e.static <S extends Interpretation<PlBeliefSet,
PlFormula>>
ProbabilityDistribution<S>ProbabilityDistribution.getUniformDistribution
(Set<S> interpretations, Signature sig) Returns the uniform distribution on the given interpretations.Modifier and TypeMethodDescriptionProbabilityDistribution.probability
(PlFormula f) Returns the probability of the given formulaModifier and TypeMethodDescriptionProbabilityDistribution.probability
(Interpretation<PlBeliefSet, PlFormula> w) Gets the probability of the given Herbrand interpretation (this is just an alias for get(Object o). -
Uses of PlFormula in org.tweetyproject.logics.pcl.syntax
ModifierConstructorDescriptionProbabilisticConditional
(PlFormula premise, PlFormula conclusion, Probability probability) Creates a new probabilistic conditional with the given premise, conclusion, and probability.ProbabilisticConditional
(PlFormula conclusion, Probability probability) Creates a new probabilistic conditional with a tautological premise and given conclusion and probability. -
Uses of PlFormula in org.tweetyproject.logics.pl.analysis
Modifier and TypeMethodDescriptionSimplePlInterpolantEnumerator.getStrongestInterpolant
(Collection<PlFormula> k1, Collection<PlFormula> k2) SimplePlInterpolantEnumerator.getWeakestInterpolant
(Collection<PlFormula> k1, Collection<PlFormula> k2) Modifier and TypeMethodDescriptionstatic InconsistencyMeasure<BeliefSet<PlFormula,
?>> InconsistencyMeasureFactory.getInconsistencyMeasure
(InconsistencyMeasureFactory.Measure im) Creates a new inconsistency measure of the given type with default settings.SimplePlInterpolantEnumerator.getInterpolants
(Collection<PlFormula> k1, Collection<PlFormula> k2) IcebergInconsistencyMeasure.getStarConflicts
(Collection<PlFormula> beliefSet) Computes all *-conflicts of a given belief base.Modifier and TypeMethodDescriptiondouble
PossibleWorldDistance.distance
(PlFormula f, PossibleWorld b) boolean
SimplePlInterpolantEnumerator.isInterpolant
(PlFormula candidate, Collection<PlFormula> k1, Collection<PlFormula> k2) Modifier and TypeMethodDescriptionSimplePlInterpolantEnumerator.getInterpolants
(Collection<PlFormula> k1, Collection<PlFormula> k2) FuzzyInconsistencyMeasure.getOptimalInterpretation
(Collection<PlFormula> formulas) Returns an optimal interpretation as a witness for the inconsistency value.ContensionSatInconsistencyMeasure.getSATEncoding
(Collection<PlFormula> kb, int upper_bound) DHitSatInconsistencyMeasure.getSATEncoding
(Collection<PlFormula> kb, int upper_bound) DMaxSatInconsistencyMeasure.getSATEncoding
(Collection<PlFormula> kb, int upper_bound) DSumSatInconsistencyMeasure.getSATEncoding
(Collection<PlFormula> kb, int upper_bound) IcebergInconsistencyMeasure.getStarConflicts
(Collection<PlFormula> beliefSet) Computes all *-conflicts of a given belief base.SimplePlInterpolantEnumerator.getStrongestInterpolant
(Collection<PlFormula> k1, Collection<PlFormula> k2) SimplePlInterpolantEnumerator.getWeakestInterpolant
(Collection<PlFormula> k1, Collection<PlFormula> k2) ContensionInconsistencyMeasure.inconsistencyMeasure
(Collection<PlFormula> formulas) ContensionSatInconsistencyMeasure.inconsistencyMeasure
(Collection<PlFormula> kb) DHitSatInconsistencyMeasure.inconsistencyMeasure
(Collection<PlFormula> kb) DMaxSatInconsistencyMeasure.inconsistencyMeasure
(Collection<PlFormula> kb) DSumSatInconsistencyMeasure.inconsistencyMeasure
(Collection<PlFormula> kb) FbInconsistencyMeasure.inconsistencyMeasure
(Collection<PlFormula> formulas) FuzzyInconsistencyMeasure.inconsistencyMeasure
(Collection<PlFormula> formulas) HsSatInconsistencyMeasure.inconsistencyMeasure
(Collection<PlFormula> kb) IcebergInconsistencyMeasure.inconsistencyMeasure
(Collection<PlFormula> formulas) MusVarInconsistencyMeasure.inconsistencyMeasure
(Collection<PlFormula> formulas) PmInconsistencyMeasure.inconsistencyMeasure
(Collection<PlFormula> formulas) boolean
SimplePlInterpolantEnumerator.isInterpolant
(PlFormula candidate, Collection<PlFormula> k1, Collection<PlFormula> k2) -
Uses of PlFormula in org.tweetyproject.logics.pl.parser
Modifier and TypeMethodDescriptionstatic Parser<PlBeliefSet,
PlFormula> PlParserFactory.getParserForFormat
(PlParserFactory.Format f) Retrieves an appropriate parser for the given format. -
Uses of PlFormula in org.tweetyproject.logics.pl.postulates
Modifier and TypeMethodDescriptionboolean
ImAdjunctionInvariance.isApplicable
(Collection<PlFormula> kb) boolean
ImAttenuation.isApplicable
(Collection<PlFormula> kb) boolean
ImConsistency.isApplicable
(Collection<PlFormula> kb) boolean
ImContradiction.isApplicable
(Collection<PlFormula> kb) boolean
ImDominance.isApplicable
(Collection<PlFormula> kb) boolean
ImEqualConflict.isApplicable
(Collection<PlFormula> kb) boolean
ImExchange.isApplicable
(Collection<PlFormula> kb) boolean
ImFreeFormulaDilution.isApplicable
(Collection<PlFormula> kb) boolean
ImFreeFormulaIndependence.isApplicable
(Collection<PlFormula> kb) boolean
ImIrrelevanceOfSyntax.isApplicable
(Collection<PlFormula> kb) boolean
ImMINormalization.isApplicable
(Collection<PlFormula> kb) boolean
ImMISeparability.isApplicable
(Collection<PlFormula> kb) boolean
ImMonotony.isApplicable
(Collection<PlFormula> kb) boolean
ImNormalization.isApplicable
(Collection<PlFormula> kb) boolean
ImPenalty.isApplicable
(Collection<PlFormula> kb) abstract boolean
ImPostulate.isApplicable
(Collection<PlFormula> kb) boolean
ImSafeFormulaIndependence.isApplicable
(Collection<PlFormula> kb) boolean
ImSuperAdditivity.isApplicable
(Collection<PlFormula> kb) boolean
ImWeakDominance.isApplicable
(Collection<PlFormula> kb) boolean
ImAdjunctionInvariance.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImAdjunctionInvariance.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImAttenuation.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImAttenuation.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImConsistency.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImConsistency.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImContradiction.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImContradiction.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImDominance.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImDominance.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImEqualConflict.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImEqualConflict.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImExchange.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImExchange.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImFreeFormulaDilution.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImFreeFormulaDilution.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImFreeFormulaIndependence.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImFreeFormulaIndependence.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImIrrelevanceOfSyntax.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImIrrelevanceOfSyntax.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImMINormalization.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImMINormalization.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImMISeparability.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImMISeparability.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImMonotony.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImMonotony.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImNormalization.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImNormalization.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImPenalty.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImPenalty.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImPostulate.isSatisfied
(Collection<PlFormula> kb, PostulateEvaluatable<PlFormula> ev) boolean
ImPostulate.isSatisfied
(Collection<PlFormula> kb, PostulateEvaluatable<PlFormula> ev) abstract boolean
ImPostulate.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) abstract boolean
ImPostulate.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImSafeFormulaIndependence.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImSafeFormulaIndependence.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImSuperAdditivity.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImSuperAdditivity.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImWeakDominance.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) boolean
ImWeakDominance.isSatisfied
(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev) -
Uses of PlFormula in org.tweetyproject.logics.pl.reasoner
Modifier and TypeMethodDescriptionAbstractPlReasoner.getKernels
(Collection<PlFormula> formulas, PlFormula formula) Modifier and TypeMethodDescriptionAbstractPlReasoner.getKernels
(Collection<PlFormula> formulas, PlFormula formula) boolean
AbstractPlReasoner.isEquivalent
(PlFormula p1, PlFormula p2) Checks whether the two formulas are equivalentabstract Boolean
AbstractPlReasoner.query
(PlBeliefSet beliefbase, PlFormula formula) boolean
Checks whether the first formula entails the second.SatReasoner.query
(PlBeliefSet beliefbase, PlFormula formula) SimplePlReasoner.query
(PlBeliefSet beliefbase, PlFormula formula) Modifier and TypeMethodDescriptionAbstractPlReasoner.getKernels
(Collection<PlFormula> formulas, PlFormula formula) -
Uses of PlFormula in org.tweetyproject.logics.pl.sat
Modifier and TypeMethodDescriptionSatSolver.convertToDimacs
(Collection<PlFormula> formulas) Converts the given set of formulas to their string representation in Dimacs CNF.static AbstractMusEnumerator<PlFormula>
PlMusEnumerator.getDefaultEnumerator()
Returns the default MUS enumerator.
If a default MUS enumerator has been configured this enumerator is returned by this method.CmdLineSatSolver.getWitness
(Collection<PlFormula> formulas) MaxSatSolver.getWitness
(Collection<PlFormula> formulas) abstract Interpretation<PlBeliefSet,
PlFormula> MaxSatSolver.getWitness
(Collection<PlFormula> hardConstraints, Map<PlFormula, Integer> softConstraints) Returns an interpretation with maximal weight on the soft constraints (or null if the hard constraints are not satisfiable)OpenWboSolver.getWitness
(Collection<PlFormula> hardConstraints, Map<PlFormula, Integer> softConstraints) Sat4jSolver.getWitness
(Collection<PlFormula> formulas) abstract Interpretation<PlBeliefSet,
PlFormula> SatSolver.getWitness
(Collection<PlFormula> formulas) If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.SatSolver.getWitness
(BeliefSet<PlFormula, ?> bs) SatSolver.getWitness
(PlFormula formula) SimpleDpllSolver.getWitness
(Collection<PlFormula> formulas) MarcoMusEnumerator.minimalInconsistentSubsets
(Collection<PlFormula> formulas) MimusMusEnumerator.minimalInconsistentSubsets
(Collection<PlFormula> formulas) abstract Collection<Collection<PlFormula>>
PlMusEnumerator.minimalInconsistentSubsets
(Collection<PlFormula> formulas) Modifier and TypeMethodDescriptionSatSolver.getWitness
(PlFormula formula) boolean
SatSolver.isConsistent
(PlFormula formula) Modifier and TypeMethodDescriptionSatSolver.convertToDimacs
(Collection<PlFormula> formulas) Converts the given set of formulas to their string representation in Dimacs CNF.static String
SatSolver.convertToDimacs
(Collection<PlFormula> formulas, List<Proposition> props) Converts the given set of formulas to their string representation in Dimacs CNF.static int
MaxSatSolver.costOf
(Interpretation<PlBeliefSet, PlFormula> interpretation, Collection<PlFormula> hardConstraints, Map<PlFormula, Integer> softConstraints) Returns the cost of the given interpretation, i.e.static int
MaxSatSolver.costOf
(Interpretation<PlBeliefSet, PlFormula> interpretation, Collection<PlFormula> hardConstraints, Map<PlFormula, Integer> softConstraints) Returns the cost of the given interpretation, i.e.static int
MaxSatSolver.costOf
(Interpretation<PlBeliefSet, PlFormula> interpretation, Collection<PlFormula> hardConstraints, Map<PlFormula, Integer> softConstraints) Returns the cost of the given interpretation, i.e.CmdLineSatSolver.getWitness
(Collection<PlFormula> formulas) MaxSatSolver.getWitness
(Collection<PlFormula> formulas) abstract Interpretation<PlBeliefSet,
PlFormula> MaxSatSolver.getWitness
(Collection<PlFormula> hardConstraints, Map<PlFormula, Integer> softConstraints) Returns an interpretation with maximal weight on the soft constraints (or null if the hard constraints are not satisfiable)abstract Interpretation<PlBeliefSet,
PlFormula> MaxSatSolver.getWitness
(Collection<PlFormula> hardConstraints, Map<PlFormula, Integer> softConstraints) Returns an interpretation with maximal weight on the soft constraints (or null if the hard constraints are not satisfiable)OpenWboSolver.getWitness
(Collection<PlFormula> hardConstraints, Map<PlFormula, Integer> softConstraints) OpenWboSolver.getWitness
(Collection<PlFormula> hardConstraints, Map<PlFormula, Integer> softConstraints) Sat4jSolver.getWitness
(Collection<PlFormula> formulas) abstract Interpretation<PlBeliefSet,
PlFormula> SatSolver.getWitness
(Collection<PlFormula> formulas) If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.SatSolver.getWitness
(BeliefSet<PlFormula, ?> bs) SimpleDpllSolver.getWitness
(Collection<PlFormula> formulas) boolean
SatSolver.isConsistent
(Collection<PlFormula> formulas) boolean
SatSolver.isConsistent
(BeliefSet<PlFormula, ?> beliefSet) boolean
CmdLineSatSolver.isSatisfiable
(Collection<PlFormula> formulas) boolean
MaxSatSolver.isSatisfiable
(Collection<PlFormula> formulas) boolean
Sat4jSolver.isSatisfiable
(Collection<PlFormula> formulas) abstract boolean
SatSolver.isSatisfiable
(Collection<PlFormula> formulas) Checks whether the given set of formulas is satisfiable.boolean
SimpleDpllSolver.isSatisfiable
(Collection<PlFormula> formulas) MarcoMusEnumerator.minimalInconsistentSubsets
(Collection<PlFormula> formulas) MimusMusEnumerator.minimalInconsistentSubsets
(Collection<PlFormula> formulas) abstract Collection<Collection<PlFormula>>
PlMusEnumerator.minimalInconsistentSubsets
(Collection<PlFormula> formulas) static void
PlMusEnumerator.setDefaultEnumerator
(AbstractMusEnumerator<PlFormula> enumerator) Sets the default MUS enumerator. -
Uses of PlFormula in org.tweetyproject.logics.pl.semantics
Modifier and TypeMethodDescriptionPossibleWorld.getCompleteConjunction
(PlSignature sig) Returns the complete conjunction representing this possible world wrt.Modifier and TypeMethodDescriptionPossibleWorldIterator.reset()
PossibleWorldIterator.reset
(Collection<? extends Formula> formulas) Modifier and TypeMethodDescriptionboolean
boolean
boolean
boolean
PriestWorld.satisfies3VL
(PlFormula formula) Determines the 3-valued truth value of the given formula.Modifier and TypeMethodDescriptionboolean
PossibleWorld.satisfies
(Collection<PlFormula> formulas) -
Uses of PlFormula in org.tweetyproject.logics.pl.syntax
Modifier and TypeClassDescriptionclass
This class captures the common functionalities of formulas with an associative operation like conjunction, disjunction, etc.class
This class represents a conjunction in propositional logic.class
A contradictory formula.class
This class represents a disjunction in propositional logic.class
This class models equivalence of propositional logic.class
This class represents an exclusive disjunction (XOR) in propositional logic.class
This class models the implication of propositional logic.class
This class models classical negation of propositional logic.class
This class represents a simple proposition in propositional logic.class
This class captures the common functionalities of the special formulas tautology and contradiction.class
A tautological formula.Modifier and TypeMethodDescriptionDisjunction.clone()
ExclusiveDisjunction.clone()
Negation.clone()
abstract PlFormula
PlFormula.clone()
Conjunction.collapseAssociativeFormulas()
Disjunction.collapseAssociativeFormulas()
Equivalence.collapseAssociativeFormulas()
ExclusiveDisjunction.collapseAssociativeFormulas()
Implication.collapseAssociativeFormulas()
Negation.collapseAssociativeFormulas()
abstract PlFormula
PlFormula.collapseAssociativeFormulas()
This method collapses all associative operations appearing in this term, e.g.Proposition.collapseAssociativeFormulas()
SpecialFormula.collapseAssociativeFormulas()
AssociativePlFormula.get
(int index) Implication.getFirstFormula()
* Get the left side formula of the implication left => right.Negation.getFormula()
Returns the formula within this negation.Implication.getSecondFormula()
Get the right side formula of the implication left => rightAssociativePlFormula.remove
(int index) Conjunction.replace
(Proposition p, PlFormula f, int i) Disjunction.replace
(Proposition p, PlFormula f, int i) Equivalence.replace
(Proposition p, PlFormula f, int i) ExclusiveDisjunction.replace
(Proposition p, PlFormula f, int i) Implication.replace
(Proposition p, PlFormula f, int i) Negation.replace
(Proposition p, PlFormula f, int i) abstract PlFormula
PlFormula.replace
(Proposition p, PlFormula f, int i) Replaces the ith instance of the proposition p by f.Proposition.replace
(Proposition p, PlFormula f, int i) SpecialFormula.replace
(Proposition p, PlFormula f, int i) PlFormula.toBlakeCanonicalForm()
This method returns this formula in Blake canonical form.PlFormula.toDnf()
This method returns this formula in disjunctive normal form (DNF).Conjunction.toNnf()
Disjunction.toNnf()
Equivalence.toNnf()
ExclusiveDisjunction.toNnf()
Implication.toNnf()
Negation.toNnf()
abstract PlFormula
PlFormula.toNnf()
This method returns this formula in negation normal form (NNF).Proposition.toNnf()
SpecialFormula.toNnf()
Conjunction.trim()
Disjunction.trim()
Equivalence.trim()
ExclusiveDisjunction.trim()
Implication.trim()
Negation.trim()
abstract PlFormula
PlFormula.trim()
Removes duplicates (identical formulas) from conjunctions and disjunctions and removes duplicate negations.Proposition.trim()
SpecialFormula.trim()
Modifier and TypeMethodDescriptionPlBeliefSet.getCanonicalOrdering()
Force ordering on belief set based on comparison of hash codes.AssociativePlFormula.getFormulas()
Equivalence.getFormulas()
Returns the formulas of the equivalence.Equivalence.getFormulas()
Returns the formulas of the equivalence.Implication.getFormulas()
Returns the formulas of the implication.Implication.getFormulas()
Returns the formulas of the implication.AssociativePlFormula.getLiterals()
Equivalence.getLiterals()
Implication.getLiterals()
Negation.getLiterals()
PlFormula.getLiterals()
Returns all literals, i.e.Proposition.getLiterals()
SpecialFormula.getLiterals()
PlFormula.getPrimeImplicants()
Returns the set of prime implicants of this formula.AssociativePlFormula.iterator()
AssociativePlFormula.listIterator()
AssociativePlFormula.listIterator
(int index) AssociativePlFormula.subList
(int fromIndex, int toIndex) Modifier and TypeMethodDescriptionvoid
boolean
boolean
Adds the specified elements to the end of this collection (optional operation).boolean
Negation.hasLowerBindingPriority
(PlFormula other) Conjunction.replace
(Proposition p, PlFormula f, int i) Disjunction.replace
(Proposition p, PlFormula f, int i) Equivalence.replace
(Proposition p, PlFormula f, int i) ExclusiveDisjunction.replace
(Proposition p, PlFormula f, int i) Implication.replace
(Proposition p, PlFormula f, int i) Negation.replace
(Proposition p, PlFormula f, int i) abstract PlFormula
PlFormula.replace
(Proposition p, PlFormula f, int i) Replaces the ith instance of the proposition p by f.Proposition.replace
(Proposition p, PlFormula f, int i) SpecialFormula.replace
(Proposition p, PlFormula f, int i) boolean
PlFormula.resolvableWith
(PlFormula other) Checks whether this formula (which must be a conjunction of literals) is resolvable with the given formula (which is also a conjunction of literals), i.e.PlFormula.resolveWith
(PlFormula other) Resolves this formula with the given one (both have to be conjunctive clauses) and returns some resolvent.void
Implication.setFirstFormula
(PlFormula left) Sets the left side formula of the implication left => right.void
Equivalence.setFormulas
(PlFormula formula1, PlFormula formula2) Sets the formulas of the equivalence.void
Implication.setFormulas
(PlFormula left, PlFormula right) Sets the formulas of the implication.void
Implication.setSecondFormula
(PlFormula right) Sets the right side formula of the implication left => rightModifier and TypeMethodDescriptionboolean
AssociativePlFormula.addAll
(int index, Collection<? extends PlFormula> c) boolean
AssociativePlFormula.addAll
(Collection<? extends PlFormula> c) static PlSignature
PlSignature.getSignature
(Collection<? extends PlFormula> formulas) Returns the set of atoms appearing in the given collection of formulas.void
Equivalence.setFormulas
(Pair<PlFormula, PlFormula> formulas) Sets the formulas of the equivalence.void
Equivalence.setFormulas
(Pair<PlFormula, PlFormula> formulas) Sets the formulas of the equivalence.void
Implication.setFormulas
(Pair<PlFormula, PlFormula> formulas) Sets the formulas of the implication.void
Implication.setFormulas
(Pair<PlFormula, PlFormula> formulas) Sets the formulas of the implication.ModifierConstructorDescriptionAssociativePlFormula
(PlFormula first, PlFormula second) Creates a new associative formula with the two given formulaeConjunction
(PlFormula first, PlFormula second) Creates a new conjunction with the two given formulaeDisjunction
(PlFormula... formulas) constructorDisjunction
(PlFormula first, PlFormula second) Creates a new disjunction with the two given formulaeEquivalence
(PlFormula a, PlFormula b) Creates a new equivalence with the given two formulasExclusiveDisjunction
(PlFormula first, PlFormula second) Creates a new exclusive disjunction with the two given formulaeImplication
(PlFormula a, PlFormula b) Creates a new implication a=>b with the two given formulasCreates a new negation with the given formula.ModifierConstructorDescriptionAssociativePlFormula
(Collection<? extends PlFormula> formulas) Creates a new associative formula with the given inner formulas.Conjunction
(Collection<? extends PlFormula> formulas) Creates a new conjunction with the given inner formulas.Disjunction
(Collection<? extends PlFormula> formulas) Creates a new disjunction with the given inner formulas.Equivalence
(Pair<PlFormula, PlFormula> formulas) Creates a new equivalence with the given pair of formulasEquivalence
(Pair<PlFormula, PlFormula> formulas) Creates a new equivalence with the given pair of formulasExclusiveDisjunction
(Collection<? extends PlFormula> formulas) Creates a new XOR formula with the given inner formulas.Implication
(Pair<PlFormula, PlFormula> formulas) Creates a new implication with the given pair of formulasImplication
(Pair<PlFormula, PlFormula> formulas) Creates a new implication with the given pair of formulasPlBeliefSet
(Collection<? extends PlFormula> formulas) Creates a new knowledge base with the given set of formulas. -
Uses of PlFormula in org.tweetyproject.logics.pl.util
Modifier and TypeMethodDescriptionCnfSampler.sampleFormula()
Returns a random formulaSyntacticRandomSampler.sampleFormula
(ProbabilityFunction<Byte> prob) Samples a single formula. -
Uses of PlFormula in org.tweetyproject.logics.pl.writer
-
Uses of PlFormula in org.tweetyproject.logics.qbf.parser
Modifier and TypeMethodDescriptionQCirParser.getOutputVariable()
QbfParser.parseFormula
(Reader reader) QCirParser.parseFormula
(Reader reader) -
Uses of PlFormula in org.tweetyproject.logics.qbf.reasoner
Modifier and TypeMethodDescriptionboolean
QbfSolver.isConsistent
(PlFormula formula) NaiveQbfReasoner.query
(PlBeliefSet beliefbase, PlFormula formula) Modifier and TypeMethodDescriptionboolean
QbfSolver.isConsistent
(Collection<PlFormula> formulas) boolean
QbfSolver.isConsistent
(BeliefSet<PlFormula, ?> beliefSet) boolean
CadetSolver.isSatisfiable
(Collection<PlFormula> kb) boolean
CaqeSolver.isSatisfiable
(Collection<PlFormula> kb) boolean
GhostQSolver.isSatisfiable
(Collection<PlFormula> kb) abstract boolean
QbfSolver.isSatisfiable
(Collection<PlFormula> formulas) Checks whether the given set of formulas is satisfiable.boolean
QuteSolver.isSatisfiable
(Collection<PlFormula> kb) -
Uses of PlFormula in org.tweetyproject.logics.qbf.semantics
Modifier and TypeMethodDescriptionQbPossibleWorld.substitute
(PlFormula f, Proposition v) Substitutes all occurrences of the proposition v with the possible truth values and returns a set of the possible substitutions.Modifier and TypeMethodDescriptionboolean
Checks whether this interpretation satisfies the given formula.QbPossibleWorld.substitute
(PlFormula f, Proposition v) Substitutes all occurrences of the proposition v with the possible truth values and returns a set of the possible substitutions.Modifier and TypeMethodDescriptionboolean
QbPossibleWorld.satisfies
(Collection<PlFormula> formulas) Checks whether this interpretation satisfies the given formula. -
Uses of PlFormula in org.tweetyproject.logics.qbf.syntax
Modifier and TypeClassDescriptionclass
This class represents existential quantification for boolean formulas.class
This class represents universal quantification for boolean formulas.Modifier and TypeMethodDescriptionExistsQuantifiedFormula.clone()
ForallQuantifiedFormula.clone()
ExistsQuantifiedFormula.collapseAssociativeFormulas()
ForallQuantifiedFormula.collapseAssociativeFormulas()
ExistsQuantifiedFormula.getFormula()
ForallQuantifiedFormula.getFormula()
ExistsQuantifiedFormula.replace
(Proposition p, PlFormula f, int i) ForallQuantifiedFormula.replace
(Proposition p, PlFormula f, int i) ExistsQuantifiedFormula.toNnf()
ForallQuantifiedFormula.toNnf()
ExistsQuantifiedFormula.trim()
ForallQuantifiedFormula.trim()
Modifier and TypeMethodDescriptionExistsQuantifiedFormula.getLiterals()
ForallQuantifiedFormula.getLiterals()
Modifier and TypeMethodDescriptionExistsQuantifiedFormula.replace
(Proposition p, PlFormula f, int i) ForallQuantifiedFormula.replace
(Proposition p, PlFormula f, int i) ModifierConstructorDescriptionExistsQuantifiedFormula
(PlFormula f, Set<Proposition> variables) Create a new existential boolean quantification.ExistsQuantifiedFormula
(PlFormula f, Proposition variable) Create a new existential boolean quantification.ForallQuantifiedFormula
(PlFormula f, Set<Proposition> variables) Create a new universal boolean quantification.ForallQuantifiedFormula
(PlFormula f, Proposition variable) Create a new universal boolean quantification. -
Uses of PlFormula in org.tweetyproject.logics.translators.adfcl
Modifier and TypeMethodDescriptionConverterADF2CL.getFormulaFromAcc
(AcceptanceCondition ac) Translate "Acceptance Condition" into "PlFormula" Recursive function: Case distinction by class name -
Uses of PlFormula in org.tweetyproject.logics.translators.adfconditional
Modifier and TypeMethodDescriptionFourValuedWorldIterator.reset()
FourValuedWorldIterator.reset
(Collection<? extends Formula> formulas) Modifier and TypeMethodDescriptionboolean
boolean
ThreeValuedWorld.satisfies3VL
(PlFormula formula) Determines the 3-valued truth value of the given formula.FourValuedWorld.satisfies4VL
(PlFormula formula) Determines the 4-valued truth value of the given formula.Modifier and TypeMethodDescriptionstatic Collection<FourValuedWorld>
CADFSemantics.gammaOperator
(ArrayList<PlFormula> statementFormulas, ArrayList<PlFormula> acceptanceFormulas, PlSignature sig, FourValuedWorld worldInput) Implementation of the gamma operator: calculate a new set of (output) interpretations given a cADF and an (input) interpretationstatic Collection<FourValuedWorld>
CADFSemantics.gammaPrimeOperator
(Collection<FourValuedWorld> inputCollection, ArrayList<PlFormula> statementFormulas, ArrayList<PlFormula> acceptanceFormulas, PlSignature sig) Implementation of the Gamma Prime Operator: Calculate the union of the Gamma Operator of all input worlds and then reduce those worlds to the least informative onesstatic boolean
CADFSemantics.isComplete
(FourValuedWorld inputWorld, Collection<FourValuedWorld> outputWorlds, ArrayList<PlFormula> statementFormulas, ArrayList<PlFormula> acceptanceFormulas) Check whether a given world constitutes a complete interpretation -
Uses of PlFormula in org.tweetyproject.logics.translators.adfpossibilistic
Modifier and TypeMethodDescriptionPossibilisticGammaOperator.sortByValue
(Map<PlFormula, Double> map) Convert an unsorted Map to a map sorted by value in ascending orderModifier and TypeMethodDescriptionPossibilityDistribution.getNecessity
(PlFormula formula) Gets the necessity measure of the given formula.PossibilityDistribution.getPossibility
(PlFormula formula) Gets the possibility measure of the given formula. -
Uses of PlFormula in org.tweetyproject.logics.translators.adfrevision
Modifier and TypeClassDescriptionclass
This class models an indecision operator for 3-valued propositional logic as proposed in [Heyninck 2020] Indecision(a) is true, if formula a is undecided Indecision(a) is false, if formula a is true or false Adapted from the class "Negation"class
This class models a weak negation for 3-valued propositional logic as proposed in [Heyninck 2020] Adapted from the class "Negation"Modifier and TypeMethodDescriptionIndecision.clone()
WeakNegation.clone()
Indecision.collapseAssociativeFormulas()
WeakNegation.collapseAssociativeFormulas()
Indecision.getFormula()
Returns the formula within this negation.WeakNegation.getFormula()
Returns the formula within this negation.PlParserThreeValued.parseFormula
(Reader reader) Indecision.replace
(Proposition p, PlFormula f, int i) WeakNegation.replace
(Proposition p, PlFormula f, int i) Indecision.toNnf()
WeakNegation.toNnf()
Indecision.trim()
WeakNegation.trim()
Modifier and TypeMethodDescriptionIndecision.getLiterals()
WeakNegation.getLiterals()
PriestWorldIterator.reset()
PriestWorldIterator.reset
(Collection<? extends Formula> formulas) Modifier and TypeMethodDescriptionboolean
Indecision.hasLowerBindingPriority
(PlFormula other) boolean
WeakNegation.hasLowerBindingPriority
(PlFormula other) Gets the rank of the given formula.Indecision.replace
(Proposition p, PlFormula f, int i) WeakNegation.replace
(Proposition p, PlFormula f, int i) boolean
PriestWorldAdapted.satisfies3VL
(PlFormula formula) Determines the 3-valued truth value of the given formula.Modifier and TypeMethodDescriptionvoid
RankingFunctionThreeValued.forceStrictness
(Set<PlFormula> formulas) Sets the rank of every interpretation i that does not satisfy the given set of formulas to RankingFunction.INFINITY.ModifierConstructorDescriptionIndecision
(PlFormula formula) Creates a new negation with the given formula.WeakNegation
(PlFormula formula) Creates a new negation with the given formula. -
Uses of PlFormula in org.tweetyproject.logics.translators.folprop
-
Uses of PlFormula in org.tweetyproject.web.services
Modifier and TypeFieldDescriptionstatic AbstractMusEnumerator<PlFormula>
InconsistencyMeasurementService.musEnumerator
The MUS enumerator configured for this service.