Package net.sf.tweety.logics.fol.syntax
Class FolFormula
- java.lang.Object
-
- net.sf.tweety.logics.commons.syntax.RelationalFormula
-
- net.sf.tweety.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
public abstract class FolFormula extends RelationalFormula
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
Constructors Constructor Description FolFormula()
-
Method Summary
Modifier and Type Method Description abstract FolFormula
clone()
Creates a deep copy of this formulaabstract RelationalFormula
collapseAssociativeFormulas()
This method collapses all associative operations appearing in this term, e.g.Conjunction
combineWithAnd(Conjunctable f)
Returns a conjunction of this and the given formula.Disjunction
combineWithOr(Disjunctable f)
RelationalFormula
complement()
java.util.Set<Variable>
getQuantifierVariables()
FolSignature
getSignature()
Returns the signature of the language of this formula.Probability
getUniformProbability()
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.FolFormula
toDnf()
Makes a disjunctive normal form of this formula.abstract FolFormula
toNnf()
Makes the negation normal form of this formula.-
Methods inherited from class net.sf.tweety.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 net.sf.tweety.logics.commons.syntax.interfaces.LogicStructure
getTerms, getTerms
-
Methods inherited from interface net.sf.tweety.logics.commons.syntax.interfaces.QuantifiedFormula
containsQuantifier, getUnboundVariables, isClosed, isClosed, isWellBound, isWellBound
-
Methods inherited from interface net.sf.tweety.logics.commons.syntax.interfaces.SimpleLogicalFormula
equals, getPredicates, hashCode, isLiteral
-
-
-
-
Method Detail
-
combineWithAnd
public Conjunction combineWithAnd(Conjunctable f)
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
public Disjunction combineWithOr(Disjunctable f)
- 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
public RelationalFormula complement()
- Specified by:
complement
in interfaceInvertable
- Specified by:
complement
in classRelationalFormula
- Returns:
- the complement of this formula.
-
getQuantifierVariables
public java.util.Set<Variable> getQuantifierVariables()
- Returns:
- a set containing all quantified variables
-
toDnf
public FolFormula toDnf()
Makes a disjunctive normal form of this formula.- Returns:
- the DNF of this formula
-
toNnf
public abstract FolFormula toNnf()
Makes the negation normal form of this formula.- Returns:
- the NNF of this formula
-
collapseAssociativeFormulas
public abstract RelationalFormula 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
public Probability 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
public abstract FolFormula substitute(Term<?> v, Term<?> t) throws java.lang.IllegalArgumentException
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:
java.lang.IllegalArgumentException
- if "v" and "t" are of different sorts (NOTE: this exception is only thrown when "v" actually appears in this formula).
-
clone
public abstract FolFormula 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
public FolSignature getSignature()
Description copied from interface:Formula
Returns the signature of the language of this formula.- Returns:
- the signature of the language of this formula.
-
-