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) |
RelationalFormula |
DefeasibleRule.substitute(Term<?> v,
Term<?> t) |
abstract RelationalFormula |
DelpRule.substitute(Term<?> v,
Term<?> t) |
RelationalFormula |
DelpFact.substitute(Term<?> v,
Term<?> t) |
Modifier and Type | Class and Description |
---|---|
class |
QuantifiedFormulaSupport<T extends RelationalFormula>
This class provides common functionalities for quantified formulas, i.e.
|
Modifier and Type | Field and Description |
---|---|
private T |
QuantifiedFormulaSupport.innerFormula
The formula this quantified formula ranges over.
|
Modifier and Type | Method and Description |
---|---|
abstract RelationalFormula |
RelationalFormula.clone() |
abstract RelationalFormula |
RelationalFormula.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 |
RelationalFormula.getFormula() |
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.
|
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 |
Equivalence
The equivalence of first-order logic.
|
class |
ExistsQuantifiedFormula
Exists-quantified first-order logic formula.
|
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 first-order logic formula.
|
class |
Implication
The implication of first-order logic.
|
class |
Negation
The classical negation of first-order logic.
|
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 |
---|---|
private Pair<RelationalFormula,RelationalFormula> |
Equivalence.formulas
The pair of formulas that are part of the equivalence.
|
private Pair<RelationalFormula,RelationalFormula> |
Equivalence.formulas
The pair of formulas that are part of the equivalence.
|
private Pair<RelationalFormula,RelationalFormula> |
Implication.formulas
The pair of formulas that are part of the implication.
|
private Pair<RelationalFormula,RelationalFormula> |
Implication.formulas
The pair of formulas that are part of the implication.
|
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 |
---|---|
RelationalFormula |
Conjunction.collapseAssociativeFormulas() |
RelationalFormula |
Equivalence.collapseAssociativeFormulas() |
abstract RelationalFormula |
FolFormula.collapseAssociativeFormulas()
This method collapses all associative operations appearing
in this term, e.g.
|
RelationalFormula |
Disjunction.collapseAssociativeFormulas() |
RelationalFormula |
Implication.collapseAssociativeFormulas() |
RelationalFormula |
FolFormula.complement() |
RelationalFormula |
AssociativeFOLFormula.get(int index) |
RelationalFormula |
AssociativeFOLFormula.remove(int index) |
RelationalFormula |
AssociativeFOLFormula.set(int index,
RelationalFormula element) |
Modifier and Type | Method and Description |
---|---|
java.util.List<RelationalFormula> |
AssociativeFOLFormula.getFormulas() |
Pair<RelationalFormula,RelationalFormula> |
Equivalence.getFormulas()
Returns the formulas of the equivalence.
|
Pair<RelationalFormula,RelationalFormula> |
Equivalence.getFormulas()
Returns the formulas of the equivalence.
|
Pair<RelationalFormula,RelationalFormula> |
Implication.getFormulas()
Returns the formulas of the implication.
|
Pair<RelationalFormula,RelationalFormula> |
Implication.getFormulas()
Returns the formulas of the implication.
|
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) |
void |
Equivalence.setFormulas(Pair<RelationalFormula,RelationalFormula> formulas)
Sets the formulas of the equivalence.
|
void |
Equivalence.setFormulas(Pair<RelationalFormula,RelationalFormula> formulas)
Sets the formulas of the equivalence.
|
void |
Implication.setFormulas(Pair<RelationalFormula,RelationalFormula> formulas)
Sets the formulas of the implication.
|
void |
Implication.setFormulas(Pair<RelationalFormula,RelationalFormula> formulas)
Sets the formulas of the implication.
|
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
|
Equivalence(RelationalFormula a,
RelationalFormula b)
Creates a new equivalence with the given two formulas
|
ExistsQuantifiedFormula(RelationalFormula folFormula,
java.util.Set<Variable> variables)
Creates a new quantified folFormula with the given folFormula and variables.
|
ExistsQuantifiedFormula(RelationalFormula folFormula,
Variable variable)
Creates a new quantified folFormula with the given folFormula and variable.
|
ForallQuantifiedFormula(RelationalFormula folFormula,
java.util.Set<Variable> variables)
Creates a new quantified folFormula with the given folFormula and variables.
|
ForallQuantifiedFormula(RelationalFormula folFormula,
Variable variable)
Creates a new quantified folFormula with the given folFormula and variable.
|
Implication(RelationalFormula a,
RelationalFormula b)
Creates a new implication a=>b with the two given formulas
|
Negation(RelationalFormula formula) |
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.
|
Equivalence(Pair<RelationalFormula,RelationalFormula> formulas)
Creates a new equivalence with the given pair of formulas
|
Equivalence(Pair<RelationalFormula,RelationalFormula> formulas)
Creates a new equivalence with the given pair of formulas
|
Implication(Pair<RelationalFormula,RelationalFormula> formulas)
Creates a new implication with the given pair of formulas
|
Implication(Pair<RelationalFormula,RelationalFormula> formulas)
Creates a new implication with the given pair of formulas
|
Modifier and Type | Method and Description |
---|---|
private java.lang.String |
Prover9Writer.printFormula(RelationalFormula f)
Creates a representation of a formula in Prover9 format.
|
private java.lang.String |
SPASSWriter.printFormula(RelationalFormula f) |
private java.lang.String |
TPTPWriter.printFormula(RelationalFormula f)
Creates a TPTP representation of a formula.
|
private java.lang.String |
SPASSWriter.printFormulas(FolBeliefSet kb,
RelationalFormula formula)
Prints the axioms declaration and conjectures declaration for a SPASS input file.
|
void |
SPASSWriter.printProblem(FolBeliefSet kb,
RelationalFormula formula)
Prints the contents of a SPASS problem file for a given knowledge base and a formula.
|
Modifier and Type | Method and Description |
---|---|
private RelationalFormula |
ModalParser.parseAtomic(java.util.List<java.lang.Object> l)
Parses a simple formula as a list of String tokens or formulas into a fol formula.
|
private RelationalFormula |
ModalParser.parseConjunction(java.util.List<java.lang.Object> l)
Parses a simple conjunction as a list of String tokens or formulas into a fol formula.
|
private RelationalFormula |
ModalParser.parseDisjunction(java.util.List<java.lang.Object> l)
Parses a disjunction as a list of String tokens or formulas into a fol formula.
|
private RelationalFormula |
ModalParser.parseEquivalence(java.util.List<java.lang.Object> l)
Parses an equivalence as a list of String tokens or formulas into a fol formula.
|
private RelationalFormula |
ModalParser.parseImplication(java.util.List<java.lang.Object> l)
Parses an implication as a list of String tokens or formulas into a fol formula.
|
private RelationalFormula |
ModalParser.parseModalization(java.util.List<java.lang.Object> l)
Parses a formula containing at least one modal operator as a list of String tokens or formulas.
|
private RelationalFormula |
ModalParser.parseNegation(java.util.List<java.lang.Object> l)
Parses a simple formula as a list of String tokens or formulas into a fol formula.
|
private RelationalFormula |
ModalParser.parseQuantification(java.util.List<java.lang.Object> l)
Parses a quantified formula as a list of String tokens or formulas.
|
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 |
Necessity.collapseAssociativeFormulas() |
RelationalFormula |
Possibility.collapseAssociativeFormulas() |
RelationalFormula |
ModalFormula.complement() |
RelationalFormula |
ModalFormula.getFormula()
Returns the inner formula of this modal formula.
|
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
|
Constructor and Description |
---|
ModalBeliefSet(java.util.Set<RelationalFormula> formulas)
Creates a new modal knowledge base with the given set of formulas.
|
Modifier and Type | Method and Description |
---|---|
private java.lang.String |
MleanCoPWriter.printFormula(RelationalFormula f)
Creates a representation of a formula in MleanCoP format.
|
private java.lang.String |
SPASSWriter.printFormula(RelationalFormula f) |
private java.lang.String |
SPASSWriter.printFormulas(ModalBeliefSet kb,
RelationalFormula formula)
Prints the axioms declaration and conjectures declaration for a SPASS input file.
|
void |
SPASSWriter.printProblem(ModalBeliefSet kb,
RelationalFormula formula)
Prints the contents of a SPASS problem file for a given knowledge base and a formula.
|
void |
MleanCoPWriter.printQuery(RelationalFormula f)
Prints the query.
|
Constructor and Description |
---|
ModalWriter(RelationalFormula formula) |
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.
|