Uses of Class
org.tweetyproject.logics.pl.syntax.PlFormula

Packages that use PlFormula

Package	Description
org.tweetyproject.action.query.syntax
org.tweetyproject.agents.dialogues
org.tweetyproject.agents.dialogues.oppmodels
org.tweetyproject.arg.aspic.ruleformulagenerator
org.tweetyproject.arg.aspic.util
org.tweetyproject.arg.caf.syntax
org.tweetyproject.arg.deductive.reasoner
org.tweetyproject.arg.deductive.semantics
org.tweetyproject.arg.deductive.syntax
org.tweetyproject.arg.deductive.util
org.tweetyproject.arg.dung.causal.syntax
org.tweetyproject.arg.dung.learning.syntax
org.tweetyproject.beliefdynamics.mas
org.tweetyproject.beliefdynamics.operators
org.tweetyproject.beliefdynamics.selectiverevision.argumentative
org.tweetyproject.logics.cl.reasoner
org.tweetyproject.logics.cl.semantics
org.tweetyproject.logics.cl.syntax
org.tweetyproject.logics.pcl.reasoner
org.tweetyproject.logics.pcl.semantics
org.tweetyproject.logics.pcl.syntax
org.tweetyproject.logics.pl.analysis
org.tweetyproject.logics.pl.parser
org.tweetyproject.logics.pl.postulates
org.tweetyproject.logics.pl.reasoner
org.tweetyproject.logics.pl.sat
org.tweetyproject.logics.pl.semantics
org.tweetyproject.logics.pl.syntax
org.tweetyproject.logics.pl.util
org.tweetyproject.logics.pl.writer
org.tweetyproject.logics.qbf.parser
org.tweetyproject.logics.qbf.reasoner
org.tweetyproject.logics.qbf.semantics
org.tweetyproject.logics.qbf.syntax
org.tweetyproject.logics.translators.adfcl
org.tweetyproject.logics.translators.adfconditional
org.tweetyproject.logics.translators.adfpossibilistic
org.tweetyproject.logics.translators.adfrevision
org.tweetyproject.logics.translators.folprop

Uses of PlFormula in org.tweetyproject.action.query.syntax

Subclasses of PlFormula in org.tweetyproject.action.query.syntax

Modifier and Type	Class	Description
class	AlwaysQuery	This class represents an always query in the action query language S.
class	HoldsQuery	This class represents a holds query in the action query language S.
class	NecessarilyQuery	This class represents a necessarily query in the action query language S.
class	QueryProposition	Action queries are represented as propositional formulas with three possible types of propositions: "holds", "always" and "necessarily" propositions.

Methods in org.tweetyproject.action.query.syntax that return PlFormula

Modifier and Type	Method	Description
PlFormula	SActionQuery.getFormula()	Retrieves the propositional formula represented by this action query.

Constructors in org.tweetyproject.action.query.syntax with parameters of type PlFormula

Modifier	Constructor	Description
	SActionQuery(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

Subclasses with type arguments of type PlFormula in org.tweetyproject.agents.dialogues

Modifier and Type	Class	Description
class	ExecutableFormulaSet	This class packs a set of formulas into an executable object.

Constructor parameters in org.tweetyproject.agents.dialogues with type arguments of type PlFormula

Modifier	Constructor	Description
	ExecutableFormulaSet(Collection<? extends PlFormula> formulas)	Creates a new set for the given formulas.

Uses of PlFormula in org.tweetyproject.agents.dialogues.oppmodels

Methods in org.tweetyproject.agents.dialogues.oppmodels that return types with arguments of type PlFormula

Modifier and Type	Method	Description
DialogueTrace<PlFormula,Collection<PlFormula>>	DeductiveEnvironment.getDialogueTrace()	Returns the current dialogue trace.
DialogueTrace<PlFormula,Collection<PlFormula>>	DeductiveEnvironment.getDialogueTrace()	Returns the current dialogue trace.

Uses of PlFormula in org.tweetyproject.arg.aspic.ruleformulagenerator

Subclasses with type arguments of type PlFormula in org.tweetyproject.arg.aspic.ruleformulagenerator

Modifier and Type	Class	Description
class	PlFormulaGenerator	Implements RuleFormulaGenerator for propositional logic.

Methods in org.tweetyproject.arg.aspic.ruleformulagenerator that return PlFormula

Modifier and Type	Method	Description
PlFormula	PlFormulaGenerator.getRuleFormula(DefeasibleInferenceRule<PlFormula> r)

Method parameters in org.tweetyproject.arg.aspic.ruleformulagenerator with type arguments of type PlFormula

Modifier and Type	Method	Description
PlFormula	PlFormulaGenerator.getRuleFormula(DefeasibleInferenceRule<PlFormula> r)

Uses of PlFormula in org.tweetyproject.arg.aspic.util

Methods in org.tweetyproject.arg.aspic.util that return types with arguments of type PlFormula

Modifier and Type	Method	Description
AspicArgumentationTheory<PlFormula>	RandomAspicArgumentationTheoryGenerator.next()	Returns an ASPIC argumentation theory

Uses of PlFormula in org.tweetyproject.arg.caf.syntax

Methods in org.tweetyproject.arg.caf.syntax that return PlFormula

Modifier and Type	Method	Description
PlFormula	ConstrainedArgumentationFramework.getConstraint()	Retrieves the current propositional constraint of the framework.

Methods in org.tweetyproject.arg.caf.syntax with parameters of type PlFormula

Modifier and Type	Method	Description
boolean	ConstrainedArgumentationFramework.setConstraint(PlFormula constraint)	Sets a new propositional formula as the constraint of CAF.

Constructors in org.tweetyproject.arg.caf.syntax with parameters of type PlFormula

Modifier	Constructor	Description
	ConstrainedArgumentationFramework(Graph<Argument> graph, PlFormula constraint)	Constructor for a CAF from a graph and a propositional formula as the constraint.

Uses of PlFormula in org.tweetyproject.arg.deductive.reasoner

Classes in org.tweetyproject.arg.deductive.reasoner that implement interfaces with type arguments of type PlFormula

Modifier and Type	Class	Description
class	AbstractDeductiveArgumentationReasoner	This class contains common characteristics for deductive argumentation reasoner.

Methods in org.tweetyproject.arg.deductive.reasoner with parameters of type PlFormula

Modifier and Type	Method	Description
Double	AbstractDeductiveArgumentationReasoner.query(DeductiveKnowledgeBase kb, PlFormula f)

Uses of PlFormula in org.tweetyproject.arg.deductive.semantics

Methods in org.tweetyproject.arg.deductive.semantics that return PlFormula

Modifier and Type	Method	Description
PlFormula	DeductiveArgument.getClaim()	Returns the claim of this argument.

Methods in org.tweetyproject.arg.deductive.semantics that return types with arguments of type PlFormula

Modifier and Type	Method	Description
Collection<? extends PlFormula>	DeductiveArgument.getSupport()	Returns the support of this argument.

Constructors in org.tweetyproject.arg.deductive.semantics with parameters of type PlFormula

Modifier	Constructor	Description
	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)

Constructor parameters in org.tweetyproject.arg.deductive.semantics with type arguments of type PlFormula

Modifier	Constructor	Description
	CompilationNode(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

Classes in org.tweetyproject.arg.deductive.syntax that implement interfaces with type arguments of type PlFormula

Modifier and Type	Class	Description
class	SimplePlRule	Represents a simple propositional logic rule.
class	SimplePlRule	Represents a simple propositional logic rule.

Methods in org.tweetyproject.arg.deductive.syntax that return PlFormula

Modifier and Type	Method	Description
PlFormula	SimplePlLogicArgument.getClaim()	Returns the claim of this argument, which is a propositional logic formula.
PlFormula	SimplePlRule.getConclusion()	Retrieves the conclusion (claim) of the rule.

Methods in org.tweetyproject.arg.deductive.syntax that return types with arguments of type PlFormula

Modifier and Type	Method	Description
Collection<? extends PlFormula>	SimplePlRule.getPremise()	Retrieves the premises (support) of the rule.

Methods in org.tweetyproject.arg.deductive.syntax with parameters of type PlFormula

Modifier and Type	Method	Description
void	SimplePlRule.addPremise(PlFormula arg0)	Adds a premise to the rule.
Set<DeductiveArgument>	DeductiveKnowledgeBase.getDeductiveArguments(PlFormula claim)	Computes all deductive arguments for the given claim.
void	SimplePlRule.setConclusion(PlFormula arg0)	Sets the conclusion (claim) of the rule.

Method parameters in org.tweetyproject.arg.deductive.syntax with type arguments of type PlFormula

Modifier and Type	Method	Description
void	SimplePlRule.addPremises(Collection<? extends PlFormula> arg0)	Adds a collection of premises to the rule.

Constructors in org.tweetyproject.arg.deductive.syntax with parameters of type PlFormula

Modifier	Constructor	Description
	SimplePlLogicArgument(Collection<SimplePlRule> _support, PlFormula _claim)	Constructs a simple propositional logic argument with the given support and claim.
	SimplePlRule(PlFormula _claim)	Constructs a rule with the specified conclusion and an empty set of premises.
	SimplePlRule(PlFormula _claim, Set<PlFormula> _support)	Constructs a rule with the specified conclusion and set of premises.

Constructor parameters in org.tweetyproject.arg.deductive.syntax with type arguments of type PlFormula

Modifier	Constructor	Description
	DeductiveKnowledgeBase(Collection<? extends PlFormula> formulas)	Creates a new knowledge base with the given set of formulas.
	SimplePlRule(PlFormula _claim, Set<PlFormula> _support)	Constructs a rule with the specified conclusion and set of premises.

Uses of PlFormula in org.tweetyproject.arg.deductive.util

Classes in org.tweetyproject.arg.deductive.util that implement interfaces with type arguments of type PlFormula

Modifier and Type	Class	Description
class	RandomDeductiveKnowledgeBaseGenerator	Generates random Deductive Knowledge Bases.

Uses of PlFormula in org.tweetyproject.arg.dung.causal.syntax

Methods in org.tweetyproject.arg.dung.causal.syntax that return PlFormula

Modifier and Type	Method	Description
PlFormula	InducedArgument.getConclusion()	Returns the conclusion of this induced argument.

Methods in org.tweetyproject.arg.dung.causal.syntax that return types with arguments of type PlFormula

Modifier and Type	Method	Description
HashSet<PlFormula>	KnowledgeBase.getAssumptions()
HashSet<PlFormula>	CausalKnowledgeBase.getBeliefs()
HashSet<PlFormula>	KnowledgeBase.getBeliefs()	Retrieves all beliefs (propositional formulas) stored in this knowledge base.
HashSet<PlFormula>	CausalKnowledgeBase.getBeliefsWithoutStructuralEquations()	Retrieves all propositional formulas of this knowledge base excluding the structural equations.
HashSet<PlFormula>	CausalStatement.getConclusions()	Retrieves the conclusions of this causal statement.
HashSet<PlFormula>	CausalStatement.getPremises()	Retrieves the premises of this causal statement.
HashSet<PlFormula>	InducedArgument.getPremises()	Returns the premises of this induced argument.
HashSet<PlFormula>	CausalKnowledgeBase.getSingelAtomConclusions(Set<PlFormula> premises)	Returns all 1-atom-conclusions of this instance if the specified set of formulas is used as premises.

Methods in org.tweetyproject.arg.dung.causal.syntax with parameters of type PlFormula

Modifier and Type	Method	Description
boolean	CausalModel.add(PlFormula formula)
boolean	CausalModel.add(PlFormula... formulas)
boolean	KnowledgeBase.addAssumption(PlFormula assumption)	Adds a background assumption to this knowledge base.
boolean	InducedTheory.entails(PlFormula conclusion)	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	KnowledgeBase.entails(Set<PlFormula> premises, PlFormula conclusion)	Computes if a specified conclusion could be drawn from adding the specified premises to this instance.
boolean	KnowledgeBase.removeAssumption(PlFormula assumption)	Removes a background assumption from this knowledge base.

Method parameters in org.tweetyproject.arg.dung.causal.syntax with type arguments of type PlFormula

Modifier and Type	Method	Description
boolean	CausalModel.addAll(Collection<? extends PlFormula> formulas)
boolean	KnowledgeBase.entails(Set<PlFormula> premises, PlFormula conclusion)	Computes if a specified conclusion could be drawn from adding the specified premises to this instance.
HashSet<PlFormula>	CausalKnowledgeBase.getSingelAtomConclusions(Set<PlFormula> premises)	Returns all 1-atom-conclusions of this instance if the specified set of formulas is used as premises.

Constructors in org.tweetyproject.arg.dung.causal.syntax with parameters of type PlFormula

Modifier	Constructor	Description
	InducedArgument(CausalKnowledgeBase knowledgeBase, Set<PlFormula> premises, PlFormula conclusion)	Creates a causal argument

Constructor parameters in org.tweetyproject.arg.dung.causal.syntax with type arguments of type PlFormula

Modifier	Constructor	Description
	CausalKnowledgeBase(CausalModel facts, Set<PlFormula> assumptions)	Creates a new causal knowledge base
	CausalStatement(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 argument
	InterventionalStatement(HashSet<PlFormula> conclusions, HashMap<Proposition,Boolean> interventions, HashSet<PlFormula> premises)	Creates a new interventional causal statement.
	KnowledgeBase(Set<PlFormula> assumptions)	Constructs a knowledge base with a specified set of background assumptions.

Uses of PlFormula in org.tweetyproject.arg.dung.learning.syntax

Classes in org.tweetyproject.arg.dung.learning.syntax that implement interfaces with type arguments of type PlFormula

Modifier and Type	Class	Description
class	ClausalAttackConstraint	This class models a clausal attack constraint

Methods in org.tweetyproject.arg.dung.learning.syntax that return types with arguments of type PlFormula

Modifier and Type	Method	Description
Collection<PlFormula>	ClausalAttackConstraint.getCondition()	returns condition

Uses of PlFormula in org.tweetyproject.beliefdynamics.mas

Constructor parameters in org.tweetyproject.beliefdynamics.mas with type arguments of type PlFormula

Modifier	Constructor	Description
	AbstractCredibilityComparer(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

Subclasses with type arguments of type PlFormula in org.tweetyproject.beliefdynamics.operators

Modifier and Type	Class	Description
class	ArgumentativeRevisionOperator	This class is an exemplary instantiation of a revision operator based on deductive argumentation [Kruempelmann:2011] where several parameters have been fixed: - the inner revision is a Levi revision which bases on the random kernel contraction - the transformation function is credulous - the accumulator used for deductive argumentation is the simple accumulator - the categorizer used for deductive argumentation is the classical categorizer
class	CrMasArgumentativeRevisionOperator	This class is an exemplary instantiation of a revision operator based on deductive argumentation and credibilities where several parameters have been fixed: - the inner revision is a Levi revision which bases on the random kernel contraction - the transformation function is credulous - the accumulator used for deductive argumentation is the simple accumulator - the categorizer used for deductive argumentation is the credibility categorizer
class	CrMasSimpleRevisionOperator	This revision operator accepts only those pieces of information for revision where the credibility of the source is at least as high as the credibility of the agent which proves the complement.
class	RandomKernelContractionOperator	This class implements a simple kernel base contraction for propositional logic with an incision function that randomly selects its incisions.

Methods in org.tweetyproject.beliefdynamics.operators that return types with arguments of type PlFormula

Modifier and Type	Method	Description
Collection<PlFormula>	ArgumentativeRevisionOperator.revise(Collection<PlFormula> base, Collection<PlFormula> formulas)
Collection<InformationObject<PlFormula>>	CrMasArgumentativeRevisionOperator.revise(Collection<InformationObject<PlFormula>> base, Collection<InformationObject<PlFormula>> formulas)
Collection<InformationObject<PlFormula>>	CrMasSimpleRevisionOperator.revise(Collection<InformationObject<PlFormula>> base, Collection<InformationObject<PlFormula>> formulas)

Method parameters in org.tweetyproject.beliefdynamics.operators with type arguments of type PlFormula

Modifier and Type	Method	Description
Collection<PlFormula>	ArgumentativeRevisionOperator.revise(Collection<PlFormula> base, Collection<PlFormula> formulas)
Collection<InformationObject<PlFormula>>	CrMasArgumentativeRevisionOperator.revise(Collection<InformationObject<PlFormula>> base, Collection<InformationObject<PlFormula>> formulas)
Collection<InformationObject<PlFormula>>	CrMasSimpleRevisionOperator.revise(Collection<InformationObject<PlFormula>> base, Collection<InformationObject<PlFormula>> formulas)

Uses of PlFormula in org.tweetyproject.beliefdynamics.selectiverevision.argumentative

Classes in org.tweetyproject.beliefdynamics.selectiverevision.argumentative that implement interfaces with type arguments of type PlFormula

Modifier and Type	Class	Description
class	ArgumentativeTransformationFunction	This class implements the argumentative transformation functions proposed in [Kruempelmann:2011].

Methods in org.tweetyproject.beliefdynamics.selectiverevision.argumentative that return types with arguments of type PlFormula

Modifier and Type	Method	Description
Collection<PlFormula>	ArgumentativeTransformationFunction.transform(Collection<PlFormula> formulas)

Method parameters in org.tweetyproject.beliefdynamics.selectiverevision.argumentative with type arguments of type PlFormula

Modifier and Type	Method	Description
Collection<PlFormula>	ArgumentativeTransformationFunction.transform(Collection<PlFormula> formulas)

Uses of PlFormula in org.tweetyproject.logics.cl.reasoner

Classes in org.tweetyproject.logics.cl.reasoner that implement interfaces with type arguments of type PlFormula

Modifier and Type	Class	Description
class	AbstractConditionalLogicReasoner	Abstract ancestor for all reasoner for conditional logic.

Methods in org.tweetyproject.logics.cl.reasoner with parameters of type PlFormula

Modifier and Type	Method	Description
Boolean	AbstractConditionalLogicReasoner.query(ClBeliefSet beliefbase, PlFormula formula)

Uses of PlFormula in org.tweetyproject.logics.cl.semantics

Methods in org.tweetyproject.logics.cl.semantics with parameters of type PlFormula

Modifier and Type	Method	Description
Integer	RankingFunction.rank(PlFormula formula)	Gets the rank of the given formula.

Method parameters in org.tweetyproject.logics.cl.semantics with type arguments of type PlFormula

Modifier and Type	Method	Description
void	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

Classes in org.tweetyproject.logics.cl.syntax that implement interfaces with type arguments of type PlFormula

Modifier and Type	Class	Description
class	Conditional	This class represents a basic conditional (B|A) with formulas A,B.
class	Conditional	This class represents a basic conditional (B|A) with formulas A,B.

Methods in org.tweetyproject.logics.cl.syntax that return PlFormula

Modifier and Type	Method	Description
PlFormula	Conditional.getConclusion()

Methods in org.tweetyproject.logics.cl.syntax that return types with arguments of type PlFormula

Modifier and Type	Method	Description
Collection<PlFormula>	Conditional.getPremise()

Methods in org.tweetyproject.logics.cl.syntax with parameters of type PlFormula

Modifier and Type	Method	Description
void	Conditional.addPremise(PlFormula premise)
void	Conditional.setConclusion(PlFormula conclusion)

Method parameters in org.tweetyproject.logics.cl.syntax with type arguments of type PlFormula

Modifier and Type	Method	Description
void	Conditional.addPremises(Collection<? extends PlFormula> premises)

Constructors in org.tweetyproject.logics.cl.syntax with parameters of type PlFormula

Modifier	Constructor	Description
	Conditional(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

Classes in org.tweetyproject.logics.pcl.reasoner that implement interfaces with type arguments of type PlFormula

Modifier and Type	Class	Description
class	AbstractPclReasoner	Abstract class for all PCL reasoners.

Methods in org.tweetyproject.logics.pcl.reasoner with parameters of type PlFormula

Modifier and Type	Method	Description
abstract Double	AbstractPclReasoner.query(PclBeliefSet beliefbase, PlFormula formula)
Double	DefaultMeReasoner.query(PclBeliefSet beliefbase, PlFormula formula)
Double	GeneralizedMeReasoner.query(PclBeliefSet beliefbase, PlFormula formula)

Uses of PlFormula in org.tweetyproject.logics.pcl.semantics

Classes in org.tweetyproject.logics.pcl.semantics with type parameters of type PlFormula

Modifier and Type	Class	Description
class	ProbabilityDistribution<T extends Interpretation<PlBeliefSet,PlFormula>>	This class represents a probability distribution on some logical language

Methods in org.tweetyproject.logics.pcl.semantics with type parameters of type PlFormula

Modifier and Type	Method	Description
static <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.

Methods in org.tweetyproject.logics.pcl.semantics with parameters of type PlFormula

Modifier and Type	Method	Description
Probability	ProbabilityDistribution.probability(PlFormula f)	Returns the probability of the given formula

Method parameters in org.tweetyproject.logics.pcl.semantics with type arguments of type PlFormula

Modifier and Type	Method	Description
Probability	ProbabilityDistribution.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

Constructors in org.tweetyproject.logics.pcl.syntax with parameters of type PlFormula

Modifier	Constructor	Description
	ProbabilisticConditional(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

Subclasses with type arguments of type PlFormula in org.tweetyproject.logics.pl.analysis

Modifier and Type	Class	Description
class	CmdLineImSolver	Provides an interface to a command line based inconsistency measure analyzer
class	ContensionInconsistencyMeasure	This class implements the contension inconsistency measure, cf.
class	ContensionInconsistencyMeasurementProcess	Implements an approximation algorithm for the Contension inconsistency measure on streams.
class	FbInconsistencyMeasure	Implements the forgetting-based inconsistency measure from [Besnard.
class	FuzzyInconsistencyMeasure	This measure implements the approach presented in [Thimm, Measuring Inconsistency with Many-Valued Logics.
class	HsInconsistencyMeasurementProcess	Implements an approximation algorithm for the Hs inconsistency measure on streams.
class	IcebergInconsistencyMeasure	This class implements the inconsistency measures proposed in [De Bona, Hunter.
class	MusVarInconsistencyMeasure	This class implements the "MUS-variable based inconsistency measure" proposed in [Xiao,Ma.
class	PlWindowInconsistencyMeasurementProcess	A window inconsistency measurement process for propositional logic (this class needs to be there as no generics are allowed when instantiating a DefaultStreamBasedInconsistencyMeasure.
class	PmInconsistencyMeasure	This class implements the inconsistency measure I_{P_m} proposed in [Jabbour, Raddaoui.
class	PrimeImplicantBasedInconsistencyMeasure	computes the inconsistency measure of the
class	SatBasedInconsistencyMeasure	A common base class for inconsistency measure implementations based on SAT encodings.

Classes in org.tweetyproject.logics.pl.analysis that implement interfaces with type arguments of type PlFormula

Modifier and Type	Class	Description
class	PossibleWorldDistance	This class refines interpretation distances to distance on possible worlds.
class	SimpleMinimalModelProvider	comptes all minimal models given a set of models
class	SimplePlInterpolantEnumerator	Implements an exhaustive search approach to compute all interpolants of a knowledge base wrt.

Fields in org.tweetyproject.logics.pl.analysis with type parameters of type PlFormula

Modifier and Type	Field	Description
MinimalModelProvider<Proposition,PlBeliefSet,PlFormula>	SimplePrimeImplicantEnumerator.minModelProvider	minimal model provider
ModelProvider<?,PlBeliefSet,InterpretationSet<Proposition,PlBeliefSet,PlFormula>>	SimpleMinimalModelProvider.modelProvider	model provider

Methods in org.tweetyproject.logics.pl.analysis that return PlFormula

Modifier and Type	Method	Description
PlFormula	SimplePlInterpolantEnumerator.getStrongestInterpolant(Collection<PlFormula> k1, Collection<PlFormula> k2)
PlFormula	SimplePlInterpolantEnumerator.getWeakestInterpolant(Collection<PlFormula> k1, Collection<PlFormula> k2)

Methods in org.tweetyproject.logics.pl.analysis that return types with arguments of type PlFormula

Modifier and Type	Method	Description
Set<PlFormula>	SimplePrimeImplicantEnumerator.compressPrimeImplicants(Set<Set<PlFormula>> primeImplicants)	Return the compressed prime implicants
Set<PlFormula>	PrimeImplicantBasedInconsistencyMeasure.getConflicts(PlBeliefSet beliefSet)	Return the conflicts of the prime implicants
static InconsistencyMeasure<BeliefSet<PlFormula,?>>	InconsistencyMeasureFactory.getInconsistencyMeasure(InconsistencyMeasureFactory.Measure im)	Creates a new inconsistency measure of the given type with default settings.
Collection<PlFormula>	SimplePlInterpolantEnumerator.getInterpolants(Collection<PlFormula> k1, Collection<PlFormula> k2)
Set<InterpretationSet<Proposition,PlBeliefSet,PlFormula>>	SimpleMinimalModelProvider.getMinModels(PlBeliefSet f)
abstract List<Set<PlFormula>>	PrimeImplicantEnumerator.getPrimeImplicants(PlBeliefSet forms)	Return the prime implicants
List<Set<PlFormula>>	SimplePrimeImplicantEnumerator.getPrimeImplicants(PlBeliefSet forms)
Collection<Set<PlFormula>>	IcebergInconsistencyMeasure.getStarConflicts(Collection<PlFormula> beliefSet)	Computes all *-conflicts of a given belief base.

Methods in org.tweetyproject.logics.pl.analysis with parameters of type PlFormula

Modifier and Type	Method	Description
double	PossibleWorldDistance.distance(PlFormula f, PossibleWorld b)
Set<PossibleWorld>	SimpleMinimalModelProvider.getMinModels(PlFormula f)
boolean	SimplePlInterpolantEnumerator.isInterpolant(PlFormula candidate, Collection<PlFormula> k1, Collection<PlFormula> k2)

Method parameters in org.tweetyproject.logics.pl.analysis with type arguments of type PlFormula

Modifier and Type	Method	Description
Set<PlFormula>	SimplePrimeImplicantEnumerator.compressPrimeImplicants(Set<Set<PlFormula>> primeImplicants)	Return the compressed prime implicants
Collection<PlFormula>	SimplePlInterpolantEnumerator.getInterpolants(Collection<PlFormula> k1, Collection<PlFormula> k2)
FuzzyInterpretation	FuzzyInconsistencyMeasure.getOptimalInterpretation(Collection<PlFormula> formulas)	Returns an optimal interpretation as a witness for the inconsistency value.
PlBeliefSet	ContensionSatInconsistencyMeasure.getSATEncoding(Collection<PlFormula> kb, int upper_bound)
PlBeliefSet	DHitSatInconsistencyMeasure.getSATEncoding(Collection<PlFormula> kb, int upper_bound)
PlBeliefSet	DMaxSatInconsistencyMeasure.getSATEncoding(Collection<PlFormula> kb, int upper_bound)
PlBeliefSet	DSumSatInconsistencyMeasure.getSATEncoding(Collection<PlFormula> kb, int upper_bound)
Collection<Set<PlFormula>>	IcebergInconsistencyMeasure.getStarConflicts(Collection<PlFormula> beliefSet)	Computes all *-conflicts of a given belief base.
PlFormula	SimplePlInterpolantEnumerator.getStrongestInterpolant(Collection<PlFormula> k1, Collection<PlFormula> k2)
PlFormula	SimplePlInterpolantEnumerator.getWeakestInterpolant(Collection<PlFormula> k1, Collection<PlFormula> k2)
Double	CmdLineImSolver.inconsistencyMeasure(Collection<PlFormula> formulas)
Double	ContensionInconsistencyMeasure.inconsistencyMeasure(Collection<PlFormula> formulas)
Double	ContensionSatInconsistencyMeasure.inconsistencyMeasure(Collection<PlFormula> kb)
Double	DHitSatInconsistencyMeasure.inconsistencyMeasure(Collection<PlFormula> kb)
Double	DMaxSatInconsistencyMeasure.inconsistencyMeasure(Collection<PlFormula> kb)
Double	DSumSatInconsistencyMeasure.inconsistencyMeasure(Collection<PlFormula> kb)
Double	FbInconsistencyMeasure.inconsistencyMeasure(Collection<PlFormula> formulas)
Double	FuzzyInconsistencyMeasure.inconsistencyMeasure(Collection<PlFormula> formulas)
Double	HsSatInconsistencyMeasure.inconsistencyMeasure(Collection<PlFormula> kb)
Double	IcebergInconsistencyMeasure.inconsistencyMeasure(Collection<PlFormula> formulas)
Double	MusVarInconsistencyMeasure.inconsistencyMeasure(Collection<PlFormula> formulas)
Double	PmInconsistencyMeasure.inconsistencyMeasure(Collection<PlFormula> formulas)
Double	PrimeImplicantBasedInconsistencyMeasure.inconsistencyMeasure(Collection<PlFormula> formulas)
boolean	SimplePlInterpolantEnumerator.isInterpolant(PlFormula candidate, Collection<PlFormula> k1, Collection<PlFormula> k2)

Constructor parameters in org.tweetyproject.logics.pl.analysis with type arguments of type PlFormula

Modifier	Constructor	Description
	SimpleMinimalModelProvider(ModelProvider<?,PlBeliefSet,InterpretationSet<Proposition,PlBeliefSet,PlFormula>> modelProvider)	standard constructor with model provider
	SimplePrimeImplicantEnumerator(MinimalModelProvider<Proposition,PlBeliefSet,PlFormula> minModelProvider)	Constructor

Uses of PlFormula in org.tweetyproject.logics.pl.parser

Subclasses with type arguments of type PlFormula in org.tweetyproject.logics.pl.parser

Modifier and Type	Class	Description
class	DimacsParser	Parser a file in Dimacs format into a PlBeliefSet.
class	PlParser	This class implements a parser for propositional logic.

Methods in org.tweetyproject.logics.pl.parser that return PlFormula

Modifier and Type	Method	Description
PlFormula	PlParser.parseFormula(Reader reader)

Methods in org.tweetyproject.logics.pl.parser that return types with arguments of type PlFormula

Modifier and Type	Method	Description
static 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

Classes in org.tweetyproject.logics.pl.postulates that implement interfaces with type arguments of type PlFormula

Modifier and Type	Class	Description
class	ImPostulate	An abstract postulate for inconsistency measures in propositional logic; the ancestor of all concrete postulates.

Method parameters in org.tweetyproject.logics.pl.postulates with type arguments of type PlFormula

Modifier and Type	Method	Description
boolean	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)	Return whether the formulas are satisfied
abstract boolean	ImPostulate.isSatisfied(Collection<PlFormula> kb, BeliefSetInconsistencyMeasure<PlFormula> ev)	Return whether the formulas are satisfied
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

Classes in org.tweetyproject.logics.pl.reasoner that implement interfaces with type arguments of type PlFormula

Modifier and Type	Class	Description
class	AbstractPlReasoner	Abstract class for propositional logic reasoners.
class	AbstractPlReasoner	Abstract class for propositional logic reasoners.

Methods in org.tweetyproject.logics.pl.reasoner that return types with arguments of type PlFormula

Modifier and Type	Method	Description
Collection<Collection<PlFormula>>	AbstractPlReasoner.getKernels(Collection<PlFormula> formulas, PlFormula formula)

Methods in org.tweetyproject.logics.pl.reasoner with parameters of type PlFormula

Modifier and Type	Method	Description
Collection<Collection<PlFormula>>	AbstractPlReasoner.getKernels(Collection<PlFormula> formulas, PlFormula formula)
boolean	AbstractPlReasoner.isEquivalent(PlFormula p1, PlFormula p2)	Checks whether the two formulas are equivalent
abstract Boolean	AbstractPlReasoner.query(PlBeliefSet beliefbase, PlFormula formula)
boolean	AbstractPlReasoner.query(PlFormula formula, PlFormula formula2)	Checks whether the first formula entails the second.
Boolean	SatReasoner.query(PlBeliefSet beliefbase, PlFormula formula)
Boolean	SimplePlReasoner.query(PlBeliefSet beliefbase, PlFormula formula)

Method parameters in org.tweetyproject.logics.pl.reasoner with type arguments of type PlFormula

Modifier and Type	Method	Description
Collection<Collection<PlFormula>>	AbstractPlReasoner.getKernels(Collection<PlFormula> formulas, PlFormula formula)

Uses of PlFormula in org.tweetyproject.logics.pl.sat

Subclasses with type arguments of type PlFormula in org.tweetyproject.logics.pl.sat

Modifier and Type	Class	Description
class	PlMusEnumerator	This abstract class models a MUS enumerator for propositional logic, i.e.

Classes in org.tweetyproject.logics.pl.sat that implement interfaces with type arguments of type PlFormula

Modifier and Type	Class	Description
class	SatSolver	Abstract class for specifying SAT solvers.
class	SatSolver	Abstract class for specifying SAT solvers.
class	SimpleModelEnumerator	enumerates all models naivly
class	SimpleModelEnumerator	enumerates all models naivly

Methods in org.tweetyproject.logics.pl.sat that return types with arguments of type PlFormula

Modifier and Type	Method	Description
static Pair<String,List<PlFormula>>	PlMusEnumerator.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.
InterpretationSet<Proposition,PlBeliefSet,PlFormula>	SimpleModelEnumerator.getModel(PlBeliefSet bbase)
Set<InterpretationSet<Proposition,PlBeliefSet,PlFormula>>	SimpleModelEnumerator.getModels(Collection<PlFormula> formulas)	Return all models satifying the formulas
Collection<InterpretationSet<Proposition,PlBeliefSet,PlFormula>>	SimpleModelEnumerator.getModels(PlBeliefSet bbase)
Interpretation<PlBeliefSet,PlFormula>	CmdLineSatSolver.getWitness(Collection<PlFormula> formulas, Map<Proposition,Integer> prop_index, Map<Integer,Proposition> prop_inverted_index, List<String> additional_clauses)
Interpretation<PlBeliefSet,PlFormula>	DimacsMaxSatSolver.getWitness(Collection<PlFormula> formulas)
Interpretation<PlBeliefSet,PlFormula>	DimacsMaxSatSolver.getWitness(Collection<PlFormula> hardConstraints, Map<PlFormula,Integer> softConstraints)	interpretation of formulas
abstract Interpretation<PlBeliefSet,PlFormula>	DimacsMaxSatSolver.getWitness(Collection<PlFormula> hardConstraints, Map<PlFormula,Integer> softConstraints, Map<Proposition,Integer> prop_index, Map<Integer,Proposition> prop_inverted_index)	Return the interpetation
Interpretation<PlBeliefSet,PlFormula>	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)
Interpretation<PlBeliefSet,PlFormula>	OpenWboSolver.getWitness(Collection<PlFormula> hardConstraints, Map<PlFormula,Integer> softConstraints, Map<Proposition,Integer> prop_index, Map<Integer,Proposition> prop_inverted_index)
Interpretation<PlBeliefSet,PlFormula>	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.
Interpretation<PlBeliefSet,PlFormula>	SatSolver.getWitness(BeliefSet<PlFormula,?> bs)
Interpretation<PlBeliefSet,PlFormula>	SatSolver.getWitness(PlFormula formula)
Interpretation<PlBeliefSet,PlFormula>	SimpleDpllSolver.getWitness(Collection<PlFormula> formulas)
Collection<Collection<PlFormula>>	MarcoMusEnumerator.minimalInconsistentSubsets(Collection<PlFormula> formulas)
Collection<Collection<PlFormula>>	MimusMusEnumerator.minimalInconsistentSubsets(Collection<PlFormula> formulas)
abstract Collection<Collection<PlFormula>>	PlMusEnumerator.minimalInconsistentSubsets(Collection<PlFormula> formulas)

Methods in org.tweetyproject.logics.pl.sat with parameters of type PlFormula

Modifier and Type	Method	Description
Interpretation<PlBeliefSet,PlFormula>	SatSolver.getWitness(PlFormula formula)
boolean	SatSolver.isConsistent(PlFormula formula)

Method parameters in org.tweetyproject.logics.pl.sat with type arguments of type PlFormula

Modifier and Type	Method	Description
static List<String>	DimacsSatSolver.convertToDimacs(Collection<PlFormula> formulas)	Converts the given set of formulas to their string representation in Dimacs CNF.
static List<String>	DimacsSatSolver.convertToDimacs(Collection<PlFormula> formulas, Map<Proposition,Integer> prop_index, List<String> additional_clauses)	Convert to dimacs
static Pair<String,List<PlFormula>>	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.
Set<InterpretationSet<Proposition,PlBeliefSet,PlFormula>>	SimpleModelEnumerator.getModels(Collection<PlFormula> formulas)	Return all models satifying the formulas
Interpretation<PlBeliefSet,PlFormula>	CmdLineSatSolver.getWitness(Collection<PlFormula> formulas, Map<Proposition,Integer> prop_index, Map<Integer,Proposition> prop_inverted_index, List<String> additional_clauses)
Interpretation<PlBeliefSet,PlFormula>	DimacsMaxSatSolver.getWitness(Collection<PlFormula> formulas)
Interpretation<PlBeliefSet,PlFormula>	DimacsMaxSatSolver.getWitness(Collection<PlFormula> hardConstraints, Map<PlFormula,Integer> softConstraints)	interpretation of formulas
Interpretation<PlBeliefSet,PlFormula>	DimacsMaxSatSolver.getWitness(Collection<PlFormula> hardConstraints, Map<PlFormula,Integer> softConstraints)	interpretation of formulas
abstract Interpretation<PlBeliefSet,PlFormula>	DimacsMaxSatSolver.getWitness(Collection<PlFormula> hardConstraints, Map<PlFormula,Integer> softConstraints, Map<Proposition,Integer> prop_index, Map<Integer,Proposition> prop_inverted_index)	Return the interpetation
abstract Interpretation<PlBeliefSet,PlFormula>	DimacsMaxSatSolver.getWitness(Collection<PlFormula> hardConstraints, Map<PlFormula,Integer> softConstraints, Map<Proposition,Integer> prop_index, Map<Integer,Proposition> prop_inverted_index)	Return the interpetation
Interpretation<PlBeliefSet,PlFormula>	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)
Interpretation<PlBeliefSet,PlFormula>	OpenWboSolver.getWitness(Collection<PlFormula> hardConstraints, Map<PlFormula,Integer> softConstraints, Map<Proposition,Integer> prop_index, Map<Integer,Proposition> prop_inverted_index)
Interpretation<PlBeliefSet,PlFormula>	OpenWboSolver.getWitness(Collection<PlFormula> hardConstraints, Map<PlFormula,Integer> softConstraints, Map<Proposition,Integer> prop_index, Map<Integer,Proposition> prop_inverted_index)
Interpretation<PlBeliefSet,PlFormula>	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.
Interpretation<PlBeliefSet,PlFormula>	SatSolver.getWitness(BeliefSet<PlFormula,?> bs)
Interpretation<PlBeliefSet,PlFormula>	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)	Return "true" if the set is consistent.
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)
Collection<Collection<PlFormula>>	MarcoMusEnumerator.minimalInconsistentSubsets(Collection<PlFormula> formulas)
Collection<Collection<PlFormula>>	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

Subclasses with type arguments of type PlFormula in org.tweetyproject.logics.pl.semantics

Modifier and Type	Class	Description
class	FuzzyInterpretation	A fuzzy interpretation for propositional logic.
class	NicePossibleWorld	Wrapper for the PossibleWorld providing better representation mechanisms, it knows all the possible propositions (the signature) and therefore provides a complete representation that maps a boolean to the Proposition.
class	PossibleWorld	This class represents a possible world of propositional logic, i.e.
class	PriestWorld	A three-valued interpretation for propositional logic from Priest's three valued logic (3VL) [Priest, G.: Logic of paradox.

Classes in org.tweetyproject.logics.pl.semantics that implement interfaces with type arguments of type PlFormula

Modifier and Type	Class	Description
class	PossibleWorldIterator	Iterates effectively over all interpretation sets worlds of a given signature.

Methods in org.tweetyproject.logics.pl.semantics that return PlFormula

Modifier and Type	Method	Description
PlFormula	PossibleWorld.getCompleteConjunction(PlSignature sig)	Returns the complete conjunction representing this possible world wrt.

Methods in org.tweetyproject.logics.pl.semantics that return types with arguments of type PlFormula

Modifier and Type	Method	Description
InterpretationIterator<PlFormula,PlBeliefSet,PossibleWorld>	PossibleWorldIterator.reset()
InterpretationIterator<PlFormula,PlBeliefSet,PossibleWorld>	PossibleWorldIterator.reset(Collection<? extends Formula> formulas)
InterpretationIterator<PlFormula,PlBeliefSet,PossibleWorld>	PossibleWorldIterator.reset(Signature sig)

Methods in org.tweetyproject.logics.pl.semantics with parameters of type PlFormula

Modifier and Type	Method	Description
boolean	FuzzyInterpretation.satisfies(PlFormula formula)
boolean	NicePossibleWorld.satisfies(PlFormula formula)
boolean	PossibleWorld.satisfies(PlFormula formula)
boolean	PriestWorld.satisfies(PlFormula formula)
PriestWorld.TruthValue	PriestWorld.satisfies3VL(PlFormula formula)	Determines the 3-valued truth value of the given formula.

Method parameters in org.tweetyproject.logics.pl.semantics with type arguments of type PlFormula

Modifier and Type	Method	Description
boolean	PossibleWorld.satisfies(Collection<PlFormula> formulas)

Uses of PlFormula in org.tweetyproject.logics.pl.syntax

Subclasses of PlFormula in org.tweetyproject.logics.pl.syntax

Modifier and Type	Class	Description
class	AssociativePlFormula	This class captures the common functionalities of formulas with an associative operation like conjunction, disjunction, etc.
class	Conjunction	This class represents a conjunction in propositional logic.
class	Contradiction	A contradictory formula.
class	Disjunction	This class represents a disjunction in propositional logic.
class	Equivalence	This class models equivalence of propositional logic.
class	ExclusiveDisjunction	This class represents an exclusive disjunction (XOR) in propositional logic.
class	Implication	This class models the implication of propositional logic.
class	Negation	This class models classical negation of propositional logic.
class	Proposition	This class represents a simple proposition in propositional logic.
class	SpecialFormula	This class captures the common functionalities of the special formulas tautology and contradiction.
class	Tautology	A tautological formula.

Subclasses with type arguments of type PlFormula in org.tweetyproject.logics.pl.syntax

Modifier and Type	Class	Description
class	PlBeliefSet	This class represents a knowledge base of propositional formulae.

Classes in org.tweetyproject.logics.pl.syntax that implement interfaces with type arguments of type PlFormula

Modifier and Type	Class	Description
class	AssociativePlFormula	This class captures the common functionalities of formulas with an associative operation like conjunction, disjunction, etc.
class	AssociativePlFormula	This class captures the common functionalities of formulas with an associative operation like conjunction, disjunction, etc.

Methods in org.tweetyproject.logics.pl.syntax that return PlFormula

Modifier and Type	Method	Description
PlFormula	Disjunction.clone()
PlFormula	ExclusiveDisjunction.clone()
PlFormula	Negation.clone()
abstract PlFormula	PlFormula.clone()
PlFormula	Conjunction.collapseAssociativeFormulas()
PlFormula	Disjunction.collapseAssociativeFormulas()
PlFormula	Equivalence.collapseAssociativeFormulas()
PlFormula	ExclusiveDisjunction.collapseAssociativeFormulas()
PlFormula	Implication.collapseAssociativeFormulas()
PlFormula	Negation.collapseAssociativeFormulas()
abstract PlFormula	PlFormula.collapseAssociativeFormulas()	This method collapses all associative operations appearing in this term, e.g.
PlFormula	Proposition.collapseAssociativeFormulas()
PlFormula	SpecialFormula.collapseAssociativeFormulas()
PlFormula	AssociativePlFormula.get(int index)
PlFormula	Implication.getFirstFormula()	* Get the left side formula of the implication left => right.
PlFormula	Negation.getFormula()	Returns the formula within this negation.
PlFormula	Implication.getSecondFormula()	Get the right side formula of the implication left => right
PlFormula	AssociativePlFormula.remove(int index)
PlFormula	Conjunction.replace(Proposition p, PlFormula f, int i)
PlFormula	Disjunction.replace(Proposition p, PlFormula f, int i)
PlFormula	Equivalence.replace(Proposition p, PlFormula f, int i)
PlFormula	ExclusiveDisjunction.replace(Proposition p, PlFormula f, int i)
PlFormula	Implication.replace(Proposition p, PlFormula f, int i)
PlFormula	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.
PlFormula	Proposition.replace(Proposition p, PlFormula f, int i)
PlFormula	SpecialFormula.replace(Proposition p, PlFormula f, int i)
PlFormula	AssociativePlFormula.set(int index, PlFormula element)
PlFormula	PlFormula.toBlakeCanonicalForm()	This method returns this formula in Blake canonical form.
PlFormula	PlFormula.toDnf()	This method returns this formula in disjunctive normal form (DNF).
PlFormula	Conjunction.toNnf()
PlFormula	Disjunction.toNnf()
PlFormula	Equivalence.toNnf()
PlFormula	ExclusiveDisjunction.toNnf()
PlFormula	Implication.toNnf()
PlFormula	Negation.toNnf()
abstract PlFormula	PlFormula.toNnf()	This method returns this formula in negation normal form (NNF).
PlFormula	Proposition.toNnf()
PlFormula	SpecialFormula.toNnf()
PlFormula	Conjunction.trim()
PlFormula	Disjunction.trim()
PlFormula	Equivalence.trim()
PlFormula	ExclusiveDisjunction.trim()
PlFormula	Implication.trim()
PlFormula	Negation.trim()
abstract PlFormula	PlFormula.trim()	Removes duplicates (identical formulas) from conjunctions and disjunctions and removes duplicate negations.
PlFormula	Proposition.trim()
PlFormula	SpecialFormula.trim()

Methods in org.tweetyproject.logics.pl.syntax that return types with arguments of type PlFormula

Modifier and Type	Method	Description
List<PlFormula>	PlBeliefSet.getCanonicalOrdering()	Force ordering on belief set based on comparison of hash codes.
List<PlFormula>	AssociativePlFormula.getFormulas()
Pair<PlFormula,PlFormula>	Equivalence.getFormulas()	Returns the formulas of the equivalence.
Pair<PlFormula,PlFormula>	Equivalence.getFormulas()	Returns the formulas of the equivalence.
Pair<PlFormula,PlFormula>	Implication.getFormulas()	Returns the formulas of the implication.
Pair<PlFormula,PlFormula>	Implication.getFormulas()	Returns the formulas of the implication.
Set<PlFormula>	AssociativePlFormula.getLiterals()
Set<PlFormula>	Equivalence.getLiterals()
Set<PlFormula>	Implication.getLiterals()
Set<PlFormula>	Negation.getLiterals()
abstract Set<PlFormula>	PlFormula.getLiterals()	Returns all literals, i.e.
Set<PlFormula>	Proposition.getLiterals()
Set<PlFormula>	SpecialFormula.getLiterals()
Collection<PlFormula>	PlFormula.getPrimeImplicants()	Returns the set of prime implicants of this formula.
Iterator<PlFormula>	AssociativePlFormula.iterator()
ListIterator<PlFormula>	AssociativePlFormula.listIterator()
ListIterator<PlFormula>	AssociativePlFormula.listIterator(int index)
List<PlFormula>	AssociativePlFormula.subList(int fromIndex, int toIndex)

Methods in org.tweetyproject.logics.pl.syntax with parameters of type PlFormula

Modifier and Type	Method	Description
void	AssociativePlFormula.add(int index, PlFormula element)
boolean	AssociativePlFormula.add(PlFormula f)
boolean	AssociativePlFormula.add(PlFormula... formulas)	Adds the specified elements to the end of this collection (optional operation).
boolean	Negation.hasLowerBindingPriority(PlFormula other)	Return whether the formula has a lower binding priority
PlFormula	Conjunction.replace(Proposition p, PlFormula f, int i)
PlFormula	Disjunction.replace(Proposition p, PlFormula f, int i)
PlFormula	Equivalence.replace(Proposition p, PlFormula f, int i)
PlFormula	ExclusiveDisjunction.replace(Proposition p, PlFormula f, int i)
PlFormula	Implication.replace(Proposition p, PlFormula f, int i)
PlFormula	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.
PlFormula	Proposition.replace(Proposition p, PlFormula f, int i)
PlFormula	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.
Conjunction	PlFormula.resolveWith(PlFormula other)	Resolves this formula with the given one (both have to be conjunctive clauses) and returns some resolvent.
PlFormula	AssociativePlFormula.set(int index, PlFormula element)
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 => right

Method parameters in org.tweetyproject.logics.pl.syntax with type arguments of type PlFormula

Modifier and Type	Method	Description
boolean	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.

Constructors in org.tweetyproject.logics.pl.syntax with parameters of type PlFormula

Modifier	Constructor	Description
	AssociativePlFormula(PlFormula first, PlFormula second)	Creates a new associative formula with the two given formulae
	Conjunction(PlFormula first, PlFormula second)	Creates a new conjunction with the two given formulae
	Disjunction(PlFormula... formulas)	constructor
	Disjunction(PlFormula first, PlFormula second)	Creates a new disjunction with the two given formulae
	Equivalence(PlFormula a, PlFormula b)	Creates a new equivalence with the given two formulas
	ExclusiveDisjunction(PlFormula first, PlFormula second)	Creates a new exclusive disjunction with the two given formulae
	Implication(PlFormula a, PlFormula b)	Creates a new implication a=>b with the two given formulas
	Negation(PlFormula formula)	Creates a new negation with the given formula.

Constructor parameters in org.tweetyproject.logics.pl.syntax with type arguments of type PlFormula

Modifier	Constructor	Description
	AssociativePlFormula(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 formulas
	Equivalence(Pair<PlFormula,PlFormula> formulas)	Creates a new equivalence with the given pair of formulas
	ExclusiveDisjunction(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 formulas
	Implication(Pair<PlFormula,PlFormula> formulas)	Creates a new implication with the given pair of formulas
	PlBeliefSet(Collection<? extends PlFormula> formulas)	Creates a new knowledge base with the given set of formulas.

Uses of PlFormula in org.tweetyproject.logics.pl.util

Subclasses with type arguments of type PlFormula in org.tweetyproject.logics.pl.util

Modifier and Type	Class	Description
class	CnfSampler	A simple sampler for propositional belief bases.
class	ContensionSampler	Generates random propositional belief base with a given inconsistency measure (for the contension inconsistency measure) and of a given size.
class	HsSampler	Generates random propositional belief base with a given inconsistency measure (for the Hs inconsistency measure) and of a given size.
class	MiSampler	Generates random propositional belief base with a given inconsistency measure (for the MI inconsistency measure) and of a given size.
class	RandomSampler	This sampler generates random belief sets by selecting, for each formula a random set of possible worlds as its models.
class	RandomSatSampler	A sampler for uniform random k-SAT instances.
class	SyntacticRandomSampler	This sampler implements a random generation algorithm for generating formulas, based on the syntax tree of propositional formulas.

Classes in org.tweetyproject.logics.pl.util that implement interfaces with type arguments of type PlFormula

Modifier and Type	Class	Description
class	CanonicalIterator	Provides an iterator on all syntactically equivalent knowledge bases.
class	EnumeratingIterator	This sampler enumerates all possible propositional belief bases of the given signature.
class	SyntacticEnumeratingIterator	Generates all syntactic variations of knowledge bases
class	TextfileIterator	Enumerates all belief bases from a text file; the file contains one belief base per line.

Methods in org.tweetyproject.logics.pl.util that return PlFormula

Modifier and Type	Method	Description
PlFormula	CnfSampler.sampleFormula()	Returns a random formula
PlFormula	SyntacticRandomSampler.sampleFormula(ProbabilityFunction<Byte> prob)	Samples a single formula.

Uses of PlFormula in org.tweetyproject.logics.pl.writer

Constructors in org.tweetyproject.logics.pl.writer with parameters of type PlFormula

Modifier	Constructor	Description
	PlWriter(PlFormula plFormula)	Creates a new PlWriter for the given formula.

Uses of PlFormula in org.tweetyproject.logics.qbf.parser

Subclasses with type arguments of type PlFormula in org.tweetyproject.logics.qbf.parser

Modifier and Type	Class	Description
class	QCirParser	This class implements a parser for the QCIR (Quantified CIRcuit) format.

Methods in org.tweetyproject.logics.qbf.parser that return PlFormula

Modifier and Type	Method	Description
PlFormula	QCirParser.getOutputVariable()	Return the output gate of this QCir problem.
PlFormula	QbfParser.parseFormula(Reader reader)
PlFormula	QCirParser.parseFormula(Reader reader)

Uses of PlFormula in org.tweetyproject.logics.qbf.reasoner

Classes in org.tweetyproject.logics.qbf.reasoner that implement interfaces with type arguments of type PlFormula

Modifier and Type	Class	Description
class	QbfSolver	Abstract QBF sat solver to be implemented by concrete solvers.

Methods in org.tweetyproject.logics.qbf.reasoner with parameters of type PlFormula

Modifier and Type	Method	Description
boolean	QbfSolver.isConsistent(PlFormula formula)
Boolean	NaiveQbfReasoner.query(PlBeliefSet beliefbase, PlFormula formula)

Method parameters in org.tweetyproject.logics.qbf.reasoner with type arguments of type PlFormula

Modifier and Type	Method	Description
boolean	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

Subclasses with type arguments of type PlFormula in org.tweetyproject.logics.qbf.semantics

Modifier and Type	Class	Description
class	QbPossibleWorld	This class represents a possible world of quantified boolean logic, i.e.

Methods in org.tweetyproject.logics.qbf.semantics that return types with arguments of type PlFormula

Modifier and Type	Method	Description
Set<PlFormula>	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.

Methods in org.tweetyproject.logics.qbf.semantics with parameters of type PlFormula

Modifier and Type	Method	Description
boolean	QbPossibleWorld.satisfies(PlFormula formula)	Checks whether this interpretation satisfies the given formula.
Set<PlFormula>	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.

Method parameters in org.tweetyproject.logics.qbf.semantics with type arguments of type PlFormula

Modifier and Type	Method	Description
boolean	QbPossibleWorld.satisfies(Collection<PlFormula> formulas)	Checks whether this interpretation satisfies the given formula.

Uses of PlFormula in org.tweetyproject.logics.qbf.syntax

Subclasses of PlFormula in org.tweetyproject.logics.qbf.syntax

Modifier and Type	Class	Description
class	ExistsQuantifiedFormula	This class represents existential quantification for boolean formulas.
class	ForallQuantifiedFormula	This class represents universal quantification for boolean formulas.

Methods in org.tweetyproject.logics.qbf.syntax that return PlFormula

Modifier and Type	Method	Description
PlFormula	ExistsQuantifiedFormula.clone()
PlFormula	ForallQuantifiedFormula.clone()
PlFormula	ExistsQuantifiedFormula.collapseAssociativeFormulas()
PlFormula	ForallQuantifiedFormula.collapseAssociativeFormulas()
PlFormula	ExistsQuantifiedFormula.getFormula()	Return the quantified formula
PlFormula	ForallQuantifiedFormula.getFormula()	Return the quantified formula
PlFormula	ExistsQuantifiedFormula.replace(Proposition p, PlFormula f, int i)
PlFormula	ForallQuantifiedFormula.replace(Proposition p, PlFormula f, int i)
PlFormula	ExistsQuantifiedFormula.toNnf()
PlFormula	ForallQuantifiedFormula.toNnf()
PlFormula	ExistsQuantifiedFormula.trim()
PlFormula	ForallQuantifiedFormula.trim()

Methods in org.tweetyproject.logics.qbf.syntax that return types with arguments of type PlFormula

Modifier and Type	Method	Description
Set<PlFormula>	ExistsQuantifiedFormula.getLiterals()
Set<PlFormula>	ForallQuantifiedFormula.getLiterals()

Methods in org.tweetyproject.logics.qbf.syntax with parameters of type PlFormula

Modifier and Type	Method	Description
PlFormula	ExistsQuantifiedFormula.replace(Proposition p, PlFormula f, int i)
PlFormula	ForallQuantifiedFormula.replace(Proposition p, PlFormula f, int i)

Constructors in org.tweetyproject.logics.qbf.syntax with parameters of type PlFormula

Modifier	Constructor	Description
	ExistsQuantifiedFormula(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

Methods in org.tweetyproject.logics.translators.adfcl that return PlFormula

Modifier and Type	Method	Description
PlFormula	ConverterADF2CL.getFormulaFromAcc(AcceptanceCondition ac)	Translate "Acceptance Condition" into "PlFormula" Recursive function: Case distinction by class name

Uses of PlFormula in org.tweetyproject.logics.translators.adfconditional

Subclasses with type arguments of type PlFormula in org.tweetyproject.logics.translators.adfconditional

Modifier and Type	Class	Description
class	FourValuedWorld	This class models a four-valued interpretation for propositional logic Formulas are interpreted using completions Every atom is assigned one of the four truth values: TRUE, FALSE, UNDECIDED, INCONSISTENT
class	ThreeValuedWorld	This class models a three-valued interpretation for propositional logic Formulas are interpreted using completions Every atom is assigned one of the three truth values: TRUE, FALSE, UNDECIDED.

Classes in org.tweetyproject.logics.translators.adfconditional that implement interfaces with type arguments of type PlFormula

Modifier and Type	Class	Description
class	FourValuedWorldIterator	This class iterates over all 4-valued interpretations of a given signature.

Methods in org.tweetyproject.logics.translators.adfconditional that return types with arguments of type PlFormula

Modifier and Type	Method	Description
InterpretationIterator<PlFormula,PlBeliefSet,FourValuedWorld>	FourValuedWorldIterator.reset()
InterpretationIterator<PlFormula,PlBeliefSet,FourValuedWorld>	FourValuedWorldIterator.reset(Collection<? extends Formula> formulas)
InterpretationIterator<PlFormula,PlBeliefSet,FourValuedWorld>	FourValuedWorldIterator.reset(Signature sig)

Methods in org.tweetyproject.logics.translators.adfconditional with parameters of type PlFormula

Modifier and Type	Method	Description
boolean	FourValuedWorld.satisfies(PlFormula formula)
boolean	ThreeValuedWorld.satisfies(PlFormula formula)
ThreeValuedWorld.TruthValue	ThreeValuedWorld.satisfies3VL(PlFormula formula)	Determines the 3-valued truth value of the given formula.
FourValuedWorld.TruthValue	FourValuedWorld.satisfies4VL(PlFormula formula)	Determines the 4-valued truth value of the given formula.

Method parameters in org.tweetyproject.logics.translators.adfconditional with type arguments of type PlFormula

Modifier and Type	Method	Description
static 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) interpretation
static 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 ones
static 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

Methods in org.tweetyproject.logics.translators.adfpossibilistic that return types with arguments of type PlFormula

Modifier and Type	Method	Description
static Map<PlFormula,Double>	PossibilisticGammaOperator.sortByValue(Map<PlFormula,Double> map)	Convert an unsorted Map to a map sorted by value in ascending order

Methods in org.tweetyproject.logics.translators.adfpossibilistic with parameters of type PlFormula

Modifier and Type	Method	Description
Double	PossibilityDistribution.getNecessity(PlFormula formula)	Gets the necessity measure of the given formula.
Double	PossibilityDistribution.getPossibility(PlFormula formula)	Gets the possibility measure of the given formula.

Method parameters in org.tweetyproject.logics.translators.adfpossibilistic with type arguments of type PlFormula

Modifier and Type	Method	Description
static Map<PlFormula,Double>	PossibilisticGammaOperator.sortByValue(Map<PlFormula,Double> map)	Convert an unsorted Map to a map sorted by value in ascending order

Uses of PlFormula in org.tweetyproject.logics.translators.adfrevision

Subclasses of PlFormula in org.tweetyproject.logics.translators.adfrevision

Modifier and Type	Class	Description
class	Indecision	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	WeakNegation	This class models a weak negation for 3-valued propositional logic as proposed in [Heyninck 2020] Adapted from the class "Negation"

Subclasses with type arguments of type PlFormula in org.tweetyproject.logics.translators.adfrevision

Modifier and Type	Class	Description
class	PlParserThreeValued	Adapted from "PlParser" for the use of 3-valued logic (WeakNegation and Indecision-Operator):
class	PriestWorldAdapted	This class models a three-valued interpretation for propositional logic from Priest's three valued logic (3VL) [Priest, G.: Logic of paradox.

Classes in org.tweetyproject.logics.translators.adfrevision that implement interfaces with type arguments of type PlFormula

Modifier and Type	Class	Description
class	PriestWorldIterator	This class iterates effectively over all interpretation sets worlds of a given signature.

Methods in org.tweetyproject.logics.translators.adfrevision that return PlFormula

Modifier and Type	Method	Description
PlFormula	Indecision.clone()
PlFormula	WeakNegation.clone()
PlFormula	Indecision.collapseAssociativeFormulas()
PlFormula	WeakNegation.collapseAssociativeFormulas()
PlFormula	Indecision.getFormula()	Returns the formula within this negation.
PlFormula	WeakNegation.getFormula()	Returns the formula within this negation.
PlFormula	PlParserThreeValued.parseFormula(Reader reader)
PlFormula	Indecision.replace(Proposition p, PlFormula f, int i)
PlFormula	WeakNegation.replace(Proposition p, PlFormula f, int i)
PlFormula	Indecision.toNnf()
PlFormula	WeakNegation.toNnf()
PlFormula	Indecision.trim()
PlFormula	WeakNegation.trim()

Methods in org.tweetyproject.logics.translators.adfrevision that return types with arguments of type PlFormula

Modifier and Type	Method	Description
Set<PlFormula>	Indecision.getLiterals()
Set<PlFormula>	WeakNegation.getLiterals()
InterpretationIterator<PlFormula,PlBeliefSet,PriestWorldAdapted>	PriestWorldIterator.reset()
InterpretationIterator<PlFormula,PlBeliefSet,PriestWorldAdapted>	PriestWorldIterator.reset(Collection<? extends Formula> formulas)
InterpretationIterator<PlFormula,PlBeliefSet,PriestWorldAdapted>	PriestWorldIterator.reset(Signature sig)

Methods in org.tweetyproject.logics.translators.adfrevision with parameters of type PlFormula

Modifier and Type	Method	Description
boolean	Indecision.hasLowerBindingPriority(PlFormula other)	Return returns false
boolean	WeakNegation.hasLowerBindingPriority(PlFormula other)	Return hasLowerBindingPriority
Integer	RankingFunctionThreeValued.rank(PlFormula formula)	Gets the rank of the given formula.
PlFormula	Indecision.replace(Proposition p, PlFormula f, int i)
PlFormula	WeakNegation.replace(Proposition p, PlFormula f, int i)
boolean	PriestWorldAdapted.satisfies(PlFormula formula)
PriestWorldAdapted.TruthValue	PriestWorldAdapted.satisfies3VL(PlFormula formula)	Determines the 3-valued truth value of the given formula.

Method parameters in org.tweetyproject.logics.translators.adfrevision with type arguments of type PlFormula

Modifier and Type	Method	Description
void	RankingFunctionThreeValued.forceStrictness(Set<PlFormula> formulas)	Sets the rank of every interpretation i that does not satisfy the given set of formulas to RankingFunction.INFINITY.

Constructors in org.tweetyproject.logics.translators.adfrevision with parameters of type PlFormula

Modifier	Constructor	Description
	Indecision(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

Methods in org.tweetyproject.logics.translators.folprop that return PlFormula

Modifier and Type	Method	Description
PlFormula	FOLPropTranslator.toPropositional(FolFormula folFormula)	Return PlFormula toPropositional

Methods in org.tweetyproject.logics.translators.folprop with parameters of type PlFormula

Modifier and Type	Method	Description
FolFormula	FOLPropTranslator.toFOL(PlFormula propFormula)	Return FolFormula toFOL