Package net.sf.tweety.logics.fol.syntax
Class Conjunction
- java.lang.Object
-
- net.sf.tweety.logics.commons.syntax.RelationalFormula
-
- net.sf.tweety.logics.fol.syntax.FolFormula
-
- net.sf.tweety.logics.fol.syntax.AssociativeFolFormula
-
- net.sf.tweety.logics.fol.syntax.Conjunction
-
- All Implemented Interfaces:
java.lang.Iterable<RelationalFormula>
,java.util.Collection<RelationalFormula>
,java.util.List<RelationalFormula>
,Formula
,AssociativeFormulaSupport.AssociativeSupportBridge
,AssociativeFormula<RelationalFormula>
,ClassicalFormula
,ComplexLogicalFormula
,Conjunctable
,Disjunctable
,Invertable
,LogicStructure
,ProbabilityAware
,QuantifiedFormula
,SimpleLogicalFormula
public class Conjunction extends AssociativeFolFormula
The classical conjunction of first-order logic.- Author:
- Matthias Thimm
-
-
Constructor Summary
Constructors Constructor Description Conjunction()
Creates a new (empty) conjunction.Conjunction(java.util.Collection<? extends RelationalFormula> formulas)
Creates a new conjunction with the given inner formulas.Conjunction(RelationalFormula first, RelationalFormula second)
Creates a new conjunction with the two given formulae
-
Method Summary
Modifier and Type Method Description Conjunction
clone()
Creates a deep copy of this formulaRelationalFormula
collapseAssociativeFormulas()
This method collapses all associative operations appearing in this term, e.g.Conjunction
createEmptyFormula()
java.lang.String
getEmptySymbol()
java.lang.String
getOperatorSymbol()
boolean
isDnf()
Checks whether this formula is in disjunctive normal form.Conjunction
substitute(Term<?> v, Term<?> t)
Substitutes all occurrences of term "v" in this formula by term "t" and returns the new formula.FolFormula
toNnf()
Makes the negation normal form of this formula.-
Methods inherited from class net.sf.tweety.logics.fol.syntax.AssociativeFolFormula
add, add, add, addAll, addAll, clear, contains, containsAll, containsQuantifier, createEmptySignature, equals, get, getAtoms, getFormulas, getFormulas, getFunctors, getPredicates, getQuantifierVariables, getTerms, getTerms, getUnboundVariables, hashCode, indexOf, isClosed, isClosed, isEmpty, isLiteral, isWellBound, isWellBound, iterator, lastIndexOf, listIterator, listIterator, remove, remove, removeAll, retainAll, set, size, subList, substitute, toArray, toArray, toString
-
Methods inherited from class net.sf.tweety.logics.fol.syntax.FolFormula
combineWithAnd, combineWithOr, complement, getSignature, getUniformProbability, toDnf
-
Methods inherited from class net.sf.tweety.logics.commons.syntax.RelationalFormula
allGroundInstances, allSubstitutions, containsTermsOfType, exchange, getFormula, getPredicateCls, getSatisfactionRatio, isGround, isWellFormed
-
Methods inherited from interface net.sf.tweety.commons.Formula
getSignature
-
Methods inherited from interface net.sf.tweety.logics.commons.syntax.interfaces.SimpleLogicalFormula
getPredicateCls
-
-
-
-
Constructor Detail
-
Conjunction
public Conjunction(java.util.Collection<? extends RelationalFormula> formulas)
Creates a new conjunction with the given inner formulas.- Parameters:
formulas
- a collection of formulas.
-
Conjunction
public Conjunction()
Creates a new (empty) conjunction.
-
Conjunction
public Conjunction(RelationalFormula first, RelationalFormula second)
Creates a new conjunction with the two given formulae- Parameters:
first
- a relational formula.second
- a relational formula.
-
-
Method Detail
-
isDnf
public boolean isDnf()
Description copied from class:FolFormula
Checks whether this formula is in disjunctive normal form.- Specified by:
isDnf
in classFolFormula
- Returns:
- "true" iff this formula is in disjunctive normal form.
-
substitute
public Conjunction 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
- Overrides:
substitute
in classAssociativeFolFormula
- 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).
-
toNnf
public FolFormula toNnf()
Description copied from class:FolFormula
Makes the negation normal form of this formula.- Specified by:
toNnf
in classFolFormula
- Returns:
- the NNF of this formula
-
collapseAssociativeFormulas
public RelationalFormula collapseAssociativeFormulas()
Description copied from class:FolFormula
This method collapses all associative operations appearing in this term, e.g. every a||(b||c) becomes a||b||c.- Specified by:
collapseAssociativeFormulas
in classFolFormula
- Returns:
- the collapsed formula.
-
clone
public Conjunction 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 classFolFormula
- Returns:
- the cloned formula
-
createEmptyFormula
public Conjunction createEmptyFormula()
- Returns:
- an empty version of the AssociativeFormula
-
getOperatorSymbol
public java.lang.String getOperatorSymbol()
- Returns:
- A String representing the operator which connects two items of the associative formula.
-
getEmptySymbol
public java.lang.String getEmptySymbol()
- Returns:
- A String representing an empty version of the Associative Formula implementation
-
-