Modifier and Type | Method and Description |
---|---|
private java.lang.String |
CTransitionSystemCalculator.getAtomString(RelationalFormula f,
int t)
Utility function representing a given atom, either an actionname or a
fluentname, to be used in a rule in an extended logic program.
|
Modifier and Type | Method and Description |
---|---|
protected boolean |
CLaw.isValidDefiniteHead(RelationalFormula pl)
Checks if a propositional formula is a valid head formula for a definite
causal law, which means either a contradiction, a fluent or the negation
of a fluent.
|
Modifier and Type | Class and Description |
---|---|
class |
DefeasibleRule
This class models a defeasible rule in defeasible logic programming.
|
class |
DelpFact
This class implements a fact in defeasible logic programming which encapsulates a literal.
|
class |
DelpRule
This method is the superclass for both a strict rule and a defeasible rule in defeasible logic programming
and captures their common attributes and methods.
|
class |
StrictRule
This class models a strict rule in defeasible logic programming.
|
Modifier and Type | Method and Description |
---|---|
RelationalFormula |
StrictRule.clone() |
RelationalFormula |
DefeasibleRule.clone() |
RelationalFormula |
DelpRule.complement() |
RelationalFormula |
StrictRule.substitute(Term<?> v,
Term<?> t) |
abstract RelationalFormula |
DelpRule.substitute(Term<?> v,
Term<?> t) |
RelationalFormula |
DelpFact.substitute(Term<?> v,
Term<?> t) |
RelationalFormula |
DefeasibleRule.substitute(Term<?> v,
Term<?> t) |
Modifier and Type | Class and Description |
---|---|
class |
ModalFormula
This class models a modal formula, i.e.
|
class |
Necessity
This class models the necessity modality.
|
class |
Possibility
This class models the possibility modality.
|
Modifier and Type | Field and Description |
---|---|
private RelationalFormula |
ModalFormula.formula
The inner formula of this modal formula
|
Modifier and Type | Method and Description |
---|---|
RelationalFormula |
Possibility.clone() |
RelationalFormula |
Necessity.clone() |
RelationalFormula |
ModalFormula.complement() |
RelationalFormula |
ModalFormula.getFormula()
Returns the inner formula of this modal formula.
|
RelationalFormula |
Possibility.substitute(Term<?> v,
Term<?> t) |
RelationalFormula |
Necessity.substitute(Term<?> v,
Term<?> t) |
RelationalFormula |
ModalFormula.substitute(Term<?> v,
Term<?> t) |
Constructor and Description |
---|
ModalFormula(RelationalFormula formula) |
Necessity(RelationalFormula formula)
Creates a new necessity formula with the
given inner formula
|
Possibility(RelationalFormula formula)
Creates a new possibility formula with the
given inner formula
|
Modifier and Type | Class and Description |
---|---|
class |
AssociativeFOLFormula
This class captures the common functionalities first order associative formulas like conjunction,
disjunction, etc.
|
class |
Conjunction
The classical conjunction of first-order logic.
|
class |
Contradiction
A contradictory formula.
|
class |
Disjunction
The classical disjunction of first-order logic.
|
class |
ExistsQuantifiedFormula |
class |
FOLAtom
An atom in first-order logic, i.e.
|
class |
FolFormula
The common abstract class for formulas of first-order logic.
|
class |
ForallQuantifiedFormula
For-All quantified formula.
|
class |
Negation
The classical negation of first-order logic.
|
class |
QuantifiedFormula
The common parent of exists and forall quantified formulas, which contains common
functionalities.
|
class |
SpecialFormula
This class captures the common functionalities of the special
formulas tautology and contradiction.
|
class |
Tautology
A tautological formula.
|
Modifier and Type | Field and Description |
---|---|
protected AssociativeFormulaSupport<RelationalFormula> |
AssociativeFOLFormula.support
This helper class implements most of the common functionality of an associative
formula, so the implementation can delegate the method calls to the support
class.
|
Modifier and Type | Method and Description |
---|---|
abstract RelationalFormula |
RelationalFormula.clone() |
abstract RelationalFormula |
FolFormula.collapseAssociativeFormulas()
This method collapses all associative operations appearing
in this term, e.g.
|
RelationalFormula |
Disjunction.collapseAssociativeFormulas() |
RelationalFormula |
Conjunction.collapseAssociativeFormulas() |
abstract RelationalFormula |
RelationalFormula.complement() |
RelationalFormula |
FolFormula.complement() |
RelationalFormula |
RelationalFormula.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.
|
RelationalFormula |
AssociativeFOLFormula.get(int index) |
RelationalFormula |
RelationalFormula.getFormula() |
RelationalFormula |
AssociativeFOLFormula.remove(int index) |
RelationalFormula |
AssociativeFOLFormula.set(int index,
RelationalFormula element) |
RelationalFormula |
RelationalFormula.substitute(java.util.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.
NOTE: variables bound to quantifiers are not substituted in their inner formulas even if they appear in the map. |
abstract RelationalFormula |
RelationalFormula.substitute(Term<?> v,
Term<?> t)
Substitutes all occurrences of term "v" in this formula
by term "t" and returns the new formula.
|
Modifier and Type | Method and Description |
---|---|
java.util.Set<RelationalFormula> |
RelationalFormula.allGroundInstances(java.util.Set<Constant> constants)
Computes all ground instances of this relational formula wrt.
|
java.util.List<RelationalFormula> |
AssociativeFOLFormula.getFormulas() |
java.util.Iterator<RelationalFormula> |
AssociativeFOLFormula.iterator() |
java.util.ListIterator<RelationalFormula> |
AssociativeFOLFormula.listIterator() |
java.util.ListIterator<RelationalFormula> |
AssociativeFOLFormula.listIterator(int index) |
java.util.List<RelationalFormula> |
AssociativeFOLFormula.subList(int fromIndex,
int toIndex) |
Modifier and Type | Method and Description |
---|---|
void |
AssociativeFOLFormula.add(int index,
RelationalFormula element) |
boolean |
AssociativeFOLFormula.add(RelationalFormula e) |
RelationalFormula |
AssociativeFOLFormula.set(int index,
RelationalFormula element) |
Modifier and Type | Method and Description |
---|---|
boolean |
AssociativeFOLFormula.addAll(java.util.Collection<? extends RelationalFormula> c) |
boolean |
AssociativeFOLFormula.addAll(int index,
java.util.Collection<? extends RelationalFormula> c) |
Constructor and Description |
---|
AssociativeFOLFormula(RelationalFormula first,
RelationalFormula second)
Creates a new associative formula with the two given formulae
|
Conjunction(RelationalFormula first,
RelationalFormula second)
Creates a new conjunction with the two given formulae
|
Disjunction(RelationalFormula first,
RelationalFormula second)
Creates a new disjunction with the two given formulae
|
ExistsQuantifiedFormula(RelationalFormula folFormula,
java.util.Set<Variable> variables)
Creates a new exists-quantified formula with the given formula and variables.
|
ForallQuantifiedFormula(RelationalFormula folFormula,
java.util.Set<Variable> variables)
Creates a new for-all-quantified formula with the given formula and variables.
|
Negation(RelationalFormula formula) |
QuantifiedFormula(RelationalFormula folFormula,
java.util.Set<Variable> variables)
Creates a new quantified folFormula with the given folFormula and variables.
|
Constructor and Description |
---|
AssociativeFOLFormula(java.util.Collection<? extends RelationalFormula> formulas)
Creates a new associative formula with the given inner formulas.
|
Conjunction(java.util.Collection<? extends RelationalFormula> formulas)
Creates a new conjunction with the given inner formulas.
|
Disjunction(java.util.Collection<? extends RelationalFormula> formulas)
Creates a new disjunction with the given inner formulas.
|
Modifier and Type | Method and Description |
---|---|
private java.lang.String |
TptpWriter.printFormula(RelationalFormula f)
Creates a TPTP representation of a formula.
|
private java.lang.String |
Prover9Writer.printFormula(RelationalFormula f)
Creates a representation of a formula in prover9 format.
|
Modifier and Type | Method and Description |
---|---|
private java.lang.String |
AlchemyMlnReasoner.alchemyStringForFormula(RelationalFormula formula)
Returns the string in Alchemy syntax representing the given formula.
|
Modifier and Type | Class and Description |
---|---|
class |
MlnFormula
Instances of this class represent first-order formulas with a weight.
|
Modifier and Type | Method and Description |
---|---|
RelationalFormula |
MlnFormula.clone() |
RelationalFormula |
MlnFormula.complement() |
RelationalFormula |
MlnFormula.substitute(Term<?> v,
Term<?> t) |
Modifier and Type | Class and Description |
---|---|
class |
RelationalConditional
Instances of this class represent relational conditionals.
|
Modifier and Type | Method and Description |
---|---|
RelationalFormula |
RelationalConditional.complement() |
RelationalFormula |
RelationalConditional.substitute(Term<?> v,
Term<?> t) |
Modifier and Type | Class and Description |
---|---|
class |
DefaultRule
Models a default rule in Reiter's default logic, see [R.
|
Modifier and Type | Method and Description |
---|---|
RelationalFormula |
DefaultRule.clone() |
RelationalFormula |
DefaultRule.complement() |
RelationalFormula |
DefaultRule.substitute(Term<?> v,
Term<?> t) |
Modifier and Type | Class and Description |
---|---|
class |
RelationalProbabilisticConditional
This class represents a relational probabilistic conditional, i.e.
|
Modifier and Type | Method and Description |
---|---|
RelationalFormula |
RelationalProbabilisticConditional.substitute(Term<?> v,
Term<?> t) |
Modifier and Type | Class and Description |
---|---|
class |
NLPNot
A default negation of a first order formula, nested logic programs
only allow not quantified formulas.
|