Class FolFormula
java.lang.Object
org.tweetyproject.logics.commons.syntax.RelationalFormula
org.tweetyproject.logics.fol.syntax.FolFormula
- All Implemented Interfaces:
Formula
,ClassicalFormula
,ComplexLogicalFormula
,Conjunctable
,Disjunctable
,Invertable
,LogicStructure
,ProbabilityAware
,QuantifiedFormula
,SimpleLogicalFormula
- Direct Known Subclasses:
AssociativeFolFormula
,Equivalence
,ExistsQuantifiedFormula
,FolAtom
,ForallQuantifiedFormula
,Implication
,MlFormula
,Negation
,NLPNot
,SpecialFormula
The common abstract class for formulas of first-order logic.
NOTE: "RelationalFormula" and "FolFormula" differ in their meaning as follows:
- A relational formula is any formula over a first-order signature, i.e. even a conditional
- A first-order formula is the actual first-order formula in the classical sense.
- Author:
- Matthias Thimm, Tim Janus
-
Constructor Summary
-
Method Summary
Modifier and TypeMethodDescriptionabstract FolFormula
clone()
Creates a deep copy of this formulaabstract RelationalFormula
This method collapses all associative operations appearing in this term, e.g.Returns a conjunction of this and the given formula.Returns the signature of the language of this formula.abstract boolean
isDnf()
Checks whether this formula is in disjunctive normal form.abstract FolFormula
substitute
(Term<?> v, Term<?> t) Substitutes all occurrences of term "v" in this formula by term "t" and returns the new formula.toDnf()
Makes a disjunctive normal form of this formula.abstract FolFormula
toNnf()
Makes the negation normal form of this formula.Methods inherited from class org.tweetyproject.logics.commons.syntax.RelationalFormula
allGroundInstances, allSubstitutions, containsTermsOfType, exchange, getAtoms, getFormula, getFunctors, getPredicateCls, getSatisfactionRatio, isGround, isWellFormed, substitute, toString
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, wait, wait, wait
Methods inherited from interface org.tweetyproject.logics.commons.syntax.interfaces.LogicStructure
getTerms, getTerms
Methods inherited from interface org.tweetyproject.logics.commons.syntax.interfaces.QuantifiedFormula
containsQuantifier, getUnboundVariables, isClosed, isClosed, isWellBound, isWellBound
Methods inherited from interface org.tweetyproject.logics.commons.syntax.interfaces.SimpleLogicalFormula
equals, getPredicates, hashCode, isLiteral
-
Constructor Details
-
FolFormula
public FolFormula()
-
-
Method Details
-
combineWithAnd
Description copied from interface:Conjunctable
Returns a conjunction of this and the given formula.- Specified by:
combineWithAnd
in interfaceConjunctable
- Specified by:
combineWithAnd
in classRelationalFormula
- Parameters:
f
- a formula to be combined with AND and this.- Returns:
- a conjunction of this and the given formula.
-
combineWithOr
- Specified by:
combineWithOr
in interfaceDisjunctable
- Specified by:
combineWithOr
in classRelationalFormula
- Parameters:
f
- a formula to be combined with OR and this.- Returns:
- a disjunction of this and the given formula.
-
complement
- Specified by:
complement
in interfaceInvertable
- Specified by:
complement
in classRelationalFormula
- Returns:
- the complement of this formula.
-
getQuantifierVariables
- Returns:
- a set containing all quantified variables
-
toDnf
Makes a disjunctive normal form of this formula.- Returns:
- the DNF of this formula
-
toNnf
Makes the negation normal form of this formula.- Returns:
- the NNF of this formula
-
collapseAssociativeFormulas
This method collapses all associative operations appearing in this term, e.g. every a||(b||c) becomes a||b||c.- Returns:
- the collapsed formula.
-
getUniformProbability
- Specified by:
getUniformProbability
in interfaceProbabilityAware
- Specified by:
getUniformProbability
in classRelationalFormula
- Returns:
- this formula's probability in the uniform distribution.
-
isDnf
public abstract boolean isDnf()Checks whether this formula is in disjunctive normal form.- Returns:
- "true" iff this formula is in disjunctive normal form.
-
substitute
Description copied from class:RelationalFormula
Substitutes all occurrences of term "v" in this formula by term "t" and returns the new formula. NOTE: if "v" is a variable and bound to a quantifier then "v" is not substituted in that quantifiers inner formula.- Specified by:
substitute
in interfaceComplexLogicalFormula
- Specified by:
substitute
in classRelationalFormula
- Parameters:
v
- the term to be substituted.t
- the term to substitute.- Returns:
- a formula where every occurrence of "v" is replaced by "t".
- Throws:
IllegalArgumentException
- if "v" and "t" are of different sorts (NOTE: this exception is only thrown when "v" actually appears in this formula).
-
clone
Description copied from interface:SimpleLogicalFormula
Creates a deep copy of this formula- Specified by:
clone
in interfaceComplexLogicalFormula
- Specified by:
clone
in interfaceSimpleLogicalFormula
- Specified by:
clone
in classRelationalFormula
- Returns:
- the cloned formula
-
getSignature
Description copied from interface:Formula
Returns the signature of the language of this formula.- Returns:
- the signature of the language of this formula.
-