Package org.tweetyproject.logics.commons.syntax.interfaces

Interface ComplexLogicalFormula

All Superinterfaces:

Formula, LogicStructure, SimpleLogicalFormula

All Known Subinterfaces:

QuantifiedFormula

All Known Implementing Classes:

AbaElement, AbaRule, AggregateAtom, AggregateElement, AggregateHead, ASPAtom, ASPBodyElement, ASPElement, ASPHead, ASPLiteral, ASPRule, AssociativeFolFormula, AssociativeFormulaSupport, Assumption, ChoiceElement, ChoiceHead, ClassicalHead, ComparativeAtom, ComplexLogicalFormulaAdapter, Conjunction, Contradiction, DefaultNegation, DefaultRule, DefeasibleInferenceRule, DefeasibleRule, DelpFact, DelpRule, Disjunction, Equivalence, ExclusiveDisjunction, ExistsQuantifiedFormula, FolAtom, FolFormula, ForallQuantifiedFormula, Implication, InferenceRule, InferenceRule, MlFormula, MlnFormula, Necessity, Negation, Negation, NLPNot, NLPRule, OptimizationElement, OptimizationStatement, Possibility, RelationalConditional, RelationalFormula, RelationalProbabilisticConditional, SpecialFormula, StrictInferenceRule, StrictNegation, StrictRule, Tautology

public interface ComplexLogicalFormula
extends SimpleLogicalFormula, LogicStructure

A complex logical formula can contain arguments referred as terms, this interface provides methods to substitute and exchange those terms. It also provides utility functions like isGround() and isWellFormed().

Author:

Tim Janus, Matthias Thimm

Method Summary

Modifier and Type	Method	Description
ComplexLogicalFormula	clone()	Creates a deep copy of this formula
ComplexLogicalFormula	exchange(Term<?> v, Term<?> t)	Substitutes all occurrences of term "v" in this formula by term "t" and at the same time replaces all occurrences of term "t" by term "v" and eventually returns the new formula.
boolean	isGround()	Checks whether this formula is ground, i.e.
boolean	isWellFormed()	Checks if this formula is well formed in the logical langauge.
ComplexLogicalFormula	substitute(Map<? extends Term<?>,? extends Term<?>> map)	Substitutes all occurrences of all terms "v" in map.keyset() in this formula by map.get(v) and returns the new formula.
ComplexLogicalFormula	substitute(Term<?> v, Term<?> t)	Substitutes all occurrences of term "v" in this formula by term "t" and returns the new formula.

Methods inherited from interface org.tweetyproject.commons.Formula

getSignature

Methods inherited from interface org.tweetyproject.logics.commons.syntax.interfaces.LogicStructure

containsTermsOfType, getTerms, getTerms

Methods inherited from interface org.tweetyproject.logics.commons.syntax.interfaces.SimpleLogicalFormula

equals, getAtoms, getPredicateCls, getPredicates, hashCode, isLiteral

Method Details

substitute

ComplexLogicalFormula substitute(Term<?> v,
 Term<?> t)
                          throws IllegalArgumentException

Substitutes all occurrences of term "v" in this formula by term "t" and returns the new formula.

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

substitute

ComplexLogicalFormula substitute(Map<? extends Term<?>,? extends Term<?>> map)
                          throws IllegalArgumentException

Substitutes all occurrences of all terms "v" in map.keyset() in this formula by map.get(v) and returns the new formula.

Parameters:

map - a mapping defining which terms to be substituted.

Returns:

a formula where every term in map.keyset() has been replaced by map.get(v).

Throws:

IllegalArgumentException - if any term and its mapping are of different sorts

exchange

ComplexLogicalFormula exchange(Term<?> v,
 Term<?> t)
                        throws IllegalArgumentException

Substitutes all occurrences of term "v" in this formula by term "t" and at the same time replaces all occurrences of term "t" by term "v" and eventually returns the new formula.

Parameters:

v - a term.

t - a term.

Returns:

a new logical formula with both "v" and "t" exchanged.

Throws:

IllegalArgumentException - if "v" and "t" are of different sorts

isGround

boolean isGround()

Checks whether this formula is ground, i.e. whether there appears no variable in this formula.

Returns:

"true" if this formula is ground.

isWellFormed

boolean isWellFormed()

Checks if this formula is well formed in the logical langauge. What well- formed means is highly language dependent and the documentation of implementing sub classes shall describe the well formed term for the language they model.

Returns:

true if the formula is well-formed, false otherwise

clone

ComplexLogicalFormula clone()

Description copied from interface: SimpleLogicalFormula

Creates a deep copy of this formula

Specified by:

clone in interface SimpleLogicalFormula

Returns:

the cloned formula