Class Implication
java.lang.Object
org.tweetyproject.logics.pl.syntax.PlFormula
org.tweetyproject.logics.pl.syntax.Implication
- All Implemented Interfaces:
Formula,ClassicalFormula,Conjunctable,Disjunctable,Invertable,ProbabilityAware,SimpleLogicalFormula
This class models the implication of propositional logic.
- Author:
- Anna Gessler
-
Constructor Summary
ConstructorsConstructorDescriptionImplication(Pair<PlFormula, PlFormula> formulas) Creates a new implication with the given pair of formulasImplication(PlFormula a, PlFormula b) Creates a new implication a=>b with the two given formulas -
Method Summary
Modifier and TypeMethodDescriptionclone()Creates a deep copy of this formulaThis method collapses all associative operations appearing in this term, e.g.booleangetAtoms()Processes the set of all atoms which appear in this formula* Get the left side formula of the implication left => right.Returns the formulas of the implication.Returns all literals, i.e.getModels(PlSignature sig) Returns the set of models of this formula wrt.Processes the set of all predicates which appear in this formulaGet the right side formula of the implication left => rightReturns the signature of the language of this formula.inthashCode()intReturns the number of occurrences of the given proposition within this formulareplace(Proposition p, PlFormula f, int i) Replaces the ith instance of the proposition p by f.voidsetFirstFormula(PlFormula left) Sets the left side formula of the implication left => right.voidsetFormulas(Pair<PlFormula, PlFormula> formulas) Sets the formulas of the implication.voidsetFormulas(PlFormula left, PlFormula right) Sets the formulas of the implication.voidsetSecondFormula(PlFormula right) Sets the right side formula of the implication left => righttoCnf()This method returns this formula in conjunctive normal form (CNF).toNnf()This method returns this formula in negation normal form (NNF).toString()trim()Removes duplicates (identical formulas) from conjunctions and disjunctions and removes duplicate negations.Methods inherited from class org.tweetyproject.logics.pl.syntax.PlFormula
combineWithAnd, combineWithOr, complement, getModels, getPredicateCls, getPrimeImplicants, getUniformProbability, isClause, isConjunctiveClause, isLiteral, resolvableWith, resolveWith, toBlakeCanonicalForm, toDnf
-
Constructor Details
-
Implication
-
Implication
-
-
Method Details
-
getFormulas
-
setFormulas
-
setFormulas
-
setFirstFormula
Sets the left side formula of the implication left => right.- Parameters:
left- formula
-
setSecondFormula
Sets the right side formula of the implication left => right- Parameters:
right- formula.
-
getFirstFormula
* Get the left side formula of the implication left => right.- Returns:
- left formula
-
getSecondFormula
Get the right side formula of the implication left => right- Returns:
- right formula.
-
getAtoms
Description copied from interface:SimpleLogicalFormulaProcesses the set of all atoms which appear in this formula- Specified by:
getAtomsin interfaceSimpleLogicalFormula- Specified by:
getAtomsin classPlFormula- Returns:
- The set of all atoms
-
getLiterals
Description copied from class:PlFormulaReturns all literals, i.e. all formulas of the form "a" or "!a" where "a" is a proposition, that appear in this formula.- Specified by:
getLiteralsin classPlFormula- Returns:
- all literals appearing in this formula.
-
collapseAssociativeFormulas
Description copied from class:PlFormulaThis method collapses all associative operations appearing in this term, e.g. every a||(b||c) becomes a||b||c.- Specified by:
collapseAssociativeFormulasin classPlFormula- Returns:
- the collapsed formula.
-
getPredicates
Description copied from interface:SimpleLogicalFormulaProcesses the set of all predicates which appear in this formula- Specified by:
getPredicatesin interfaceSimpleLogicalFormula- Specified by:
getPredicatesin classPlFormula- Returns:
- all predicates that appear in this formula
-
trim
Description copied from class:PlFormulaRemoves duplicates (identical formulas) from conjunctions and disjunctions and removes duplicate negations. Simplifies equivalences and implications with equivalent formulas (A=>A, A<=>A) to tautologies. -
toNnf
-
toCnf
Description copied from class:PlFormulaThis method returns this formula in conjunctive normal form (CNF). A formula is in CNF iff it is a conjunction of disjunctions and in NNF. The CNF generated by this method is not necessarily minimal. -
getModels
Description copied from class:PlFormulaReturns the set of models of this formula wrt. the given signature. -
numberOfOccurrences
Description copied from class:PlFormulaReturns the number of occurrences of the given proposition within this formula- Specified by:
numberOfOccurrencesin classPlFormula- Parameters:
p- some proposition- Returns:
- the number of occurrences of the given proposition within this formula
-
replace
Description copied from class:PlFormulaReplaces the ith instance of the proposition p by f. -
hashCode
public int hashCode()- Specified by:
hashCodein interfaceSimpleLogicalFormula- Specified by:
hashCodein classPlFormula
-
equals
- Specified by:
equalsin interfaceSimpleLogicalFormula- Specified by:
equalsin classPlFormula
-
clone
Description copied from interface:SimpleLogicalFormulaCreates a deep copy of this formula- Specified by:
clonein interfaceSimpleLogicalFormula- Specified by:
clonein classPlFormula- Returns:
- the cloned formula
-
toString
-
getSignature
Description copied from interface:FormulaReturns the signature of the language of this formula.- Specified by:
getSignaturein interfaceFormula- Overrides:
getSignaturein classPlFormula- Returns:
- the signature of the language of this formula.
-