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) constructorSimplePlRule
(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.arg.dung.causal.syntax
Modifier and TypeMethodDescriptionKnowledgeBase.getAssumptions()
CausalKnowledgeBase.getBeliefs()
KnowledgeBase.getBeliefs()
*description missing*CausalKnowledgeBase.getBeliefsWithoutStructuralEquations()
*description missing*CausalStatement.getConclusions()
*description missing*CausalStatement.getPremises()
*description missing*InducedArgument.getPremises()
*description missing*CausalKnowledgeBase.getSingelAtomConclusions
(Set<PlFormula> premises) Returns all 1-atom-conclusions of this instance if the specified set of formulas is used as premises.Modifier and TypeMethodDescriptionboolean
boolean
boolean
KnowledgeBase.addAssumption
(PlFormula assumption) *description missing*boolean
This method checks if a specified fomula can be concluded from this instance, by checking if all stable extension contain at least one argument with the conclusion to check.boolean
Computes if a specified conclusion could be drawn from adding the specified premises to this instance.boolean
KnowledgeBase.removeAssumption
(PlFormula assumption) description missing*Modifier and TypeMethodDescriptionboolean
CausalModel.addAll
(Collection<? extends PlFormula> formulas) boolean
Computes if a specified conclusion could be drawn from adding the specified premises to this instance.CausalKnowledgeBase.getSingelAtomConclusions
(Set<PlFormula> premises) Returns all 1-atom-conclusions of this instance if the specified set of formulas is used as premises.ModifierConstructorDescriptionInducedArgument
(CausalKnowledgeBase knowledgeBase, Set<PlFormula> premises, PlFormula conclusion) Creates a causal argumentModifierConstructorDescriptionCausalKnowledgeBase
(CausalModel facts, Set<PlFormula> assumptions) Creates a new causal knowledge baseCausalStatement
(HashSet<PlFormula> conclusions, HashSet<PlFormula> premises) Creates a new causal statement.CounterfactualStatement
(HashSet<PlFormula> conclusions, HashMap<Proposition, Boolean> interventions, HashSet<PlFormula> premises) Creates a new counterfactual causal statement.InducedArgument
(CausalKnowledgeBase knowledgeBase, Set<PlFormula> premises, PlFormula conclusion) Creates a causal argumentInterventionalStatement
(HashSet<PlFormula> conclusions, HashMap<Proposition, Boolean> interventions, HashSet<PlFormula> premises) Creates a new interventional causal statement.KnowledgeBase
(Set<PlFormula> assumptions) *description missing* -
Uses of PlFormula in org.tweetyproject.arg.dung.learning.syntax
-
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 TypeFieldDescriptionSimplePrimeImplicantEnumerator.minModelProvider
minimal model providerSimpleMinimalModelProvider.modelProvider
model providerModifier and TypeMethodDescriptionSimplePlInterpolantEnumerator.getStrongestInterpolant
(Collection<PlFormula> k1, Collection<PlFormula> k2) SimplePlInterpolantEnumerator.getWeakestInterpolant
(Collection<PlFormula> k1, Collection<PlFormula> k2) Modifier and TypeMethodDescriptionSimplePrimeImplicantEnumerator.compressPrimeImplicants
(Set<Set<PlFormula>> primeImplicants) PrimeImplicantBasedInconsistencyMeasure.getConflicts
(PlBeliefSet beliefSet) static 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) SimpleMinimalModelProvider.getMinModels
(PlBeliefSet f) PrimeImplicantEnumerator.getPrimeImplicants
(PlBeliefSet forms) SimplePrimeImplicantEnumerator.getPrimeImplicants
(PlBeliefSet forms) IcebergInconsistencyMeasure.getStarConflicts
(Collection<PlFormula> beliefSet) Computes all *-conflicts of a given belief base.Modifier and TypeMethodDescriptiondouble
PossibleWorldDistance.distance
(PlFormula f, PossibleWorld b) SimpleMinimalModelProvider.getMinModels
(PlFormula f) boolean
SimplePlInterpolantEnumerator.isInterpolant
(PlFormula candidate, Collection<PlFormula> k1, Collection<PlFormula> k2) Modifier and TypeMethodDescriptionSimplePrimeImplicantEnumerator.compressPrimeImplicants
(Set<Set<PlFormula>> primeImplicants) SimplePlInterpolantEnumerator.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) CmdLineImSolver.inconsistencyMeasure
(Collection<PlFormula> formulas) 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) PrimeImplicantBasedInconsistencyMeasure.inconsistencyMeasure
(Collection<PlFormula> formulas) boolean
SimplePlInterpolantEnumerator.isInterpolant
(PlFormula candidate, Collection<PlFormula> k1, Collection<PlFormula> k2) ModifierConstructorDescriptionSimpleMinimalModelProvider
(ModelProvider<?, PlBeliefSet, InterpretationSet<Proposition, PlBeliefSet, PlFormula>> modelProvider) standard constructor with model providerSimplePrimeImplicantEnumerator
(MinimalModelProvider<Proposition, PlBeliefSet, PlFormula> minModelProvider) -
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 TypeMethodDescriptionPlMusEnumerator.convertToDimacsAndIndex
(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.SimpleModelEnumerator.getModel
(PlBeliefSet bbase) SimpleModelEnumerator.getModels
(Collection<PlFormula> formulas) SimpleModelEnumerator.getModels
(PlBeliefSet bbase) CmdLineSatSolver.getWitness
(Collection<PlFormula> formulas, Map<Proposition, Integer> prop_index, Map<Integer, Proposition> prop_inverted_index, List<String> additional_clauses) DimacsMaxSatSolver.getWitness
(Collection<PlFormula> formulas) DimacsMaxSatSolver.getWitness
(Collection<PlFormula> hardConstraints, Map<PlFormula, Integer> softConstraints) interpretation of formulasabstract Interpretation<PlBeliefSet,
PlFormula> DimacsMaxSatSolver.getWitness
(Collection<PlFormula> hardConstraints, Map<PlFormula, Integer> softConstraints, Map<Proposition, Integer> prop_index, Map<Integer, Proposition> prop_inverted_index) DimacsSatSolver.getWitness
(Collection<PlFormula> formulas) If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.abstract Interpretation<PlBeliefSet,
PlFormula> DimacsSatSolver.getWitness
(Collection<PlFormula> formulas, Map<Proposition, Integer> prop_index, Map<Integer, Proposition> prop_inverted_index, List<String> additional_clauses) If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.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, Map<Proposition, Integer> prop_index, Map<Integer, Proposition> prop_inverted_index) Sat4jSolver.getWitness
(Collection<PlFormula> formulas, Map<Proposition, Integer> prop_index, Map<Integer, Proposition> prop_inverted_index, List<String> additional_clauses) 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 TypeMethodDescriptionDimacsSatSolver.convertToDimacs
(Collection<PlFormula> formulas) Converts the given set of formulas to their string representation in Dimacs CNF.DimacsSatSolver.convertToDimacs
(Collection<PlFormula> formulas, Map<Proposition, Integer> prop_index, List<String> additional_clauses) PlMusEnumerator.convertToDimacsAndIndex
(Collection<PlFormula> formulas) 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.SimpleModelEnumerator.getModels
(Collection<PlFormula> formulas) CmdLineSatSolver.getWitness
(Collection<PlFormula> formulas, Map<Proposition, Integer> prop_index, Map<Integer, Proposition> prop_inverted_index, List<String> additional_clauses) DimacsMaxSatSolver.getWitness
(Collection<PlFormula> formulas) DimacsMaxSatSolver.getWitness
(Collection<PlFormula> hardConstraints, Map<PlFormula, Integer> softConstraints) interpretation of formulasDimacsMaxSatSolver.getWitness
(Collection<PlFormula> hardConstraints, Map<PlFormula, Integer> softConstraints) interpretation of formulasabstract Interpretation<PlBeliefSet,
PlFormula> DimacsMaxSatSolver.getWitness
(Collection<PlFormula> hardConstraints, Map<PlFormula, Integer> softConstraints, Map<Proposition, Integer> prop_index, Map<Integer, Proposition> prop_inverted_index) abstract Interpretation<PlBeliefSet,
PlFormula> DimacsMaxSatSolver.getWitness
(Collection<PlFormula> hardConstraints, Map<PlFormula, Integer> softConstraints, Map<Proposition, Integer> prop_index, Map<Integer, Proposition> prop_inverted_index) DimacsSatSolver.getWitness
(Collection<PlFormula> formulas) If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.abstract Interpretation<PlBeliefSet,
PlFormula> DimacsSatSolver.getWitness
(Collection<PlFormula> formulas, Map<Proposition, Integer> prop_index, Map<Integer, Proposition> prop_inverted_index, List<String> additional_clauses) If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.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, Map<Proposition, Integer> prop_index, Map<Integer, Proposition> prop_inverted_index) OpenWboSolver.getWitness
(Collection<PlFormula> hardConstraints, Map<PlFormula, Integer> softConstraints, Map<Proposition, Integer> prop_index, Map<Integer, Proposition> prop_inverted_index) Sat4jSolver.getWitness
(Collection<PlFormula> formulas, Map<Proposition, Integer> prop_index, Map<Integer, Proposition> prop_inverted_index, List<String> additional_clauses) 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, Map<Proposition, Integer> prop_index, List<String> additional_clauses) boolean
DimacsMaxSatSolver.isSatisfiable
(Collection<PlFormula> formulas) abstract boolean
DimacsMaxSatSolver.isSatisfiable
(Collection<PlFormula> formulas, Map<Proposition, Integer> prop_index) boolean
DimacsSatSolver.isSatisfiable
(Collection<PlFormula> formulas) Checks whether the given set of formulas is satisfiable.abstract boolean
DimacsSatSolver.isSatisfiable
(Collection<PlFormula> formulas, Map<Proposition, Integer> prop_index, List<String> additional_clauses) Checks whether the given set of formulas is satisfiable.abstract boolean
MaxSatSolver.isSatisfiable
(Collection<PlFormula> formulas) boolean
OpenWboSolver.isSatisfiable
(Collection<PlFormula> formulas, Map<Proposition, Integer> prop_index) boolean
Sat4jSolver.isSatisfiable
(Collection<PlFormula> formulas, Map<Proposition, Integer> prop_index, List<String> additional_clauses) 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.