public class DefaultRule extends RelationalFormula
Modifier and Type | Field and Description |
---|---|
private FolFormula |
conc
The conclusion of the default rule
|
private java.util.Collection<FolFormula> |
jus
The justifications of the default rule
|
private FolFormula |
pre
The prerequisite of the default rule
|
Constructor and Description |
---|
DefaultRule()
an empty Default Rule
|
DefaultRule(FolFormula pre,
java.util.Collection<FolFormula> jus,
FolFormula conc) |
DefaultRule(FolFormula pre,
FolFormula jus,
FolFormula conc) |
Modifier and Type | Method and Description |
---|---|
RelationalFormula |
clone()
Creates a deep copy of this formula
|
Conjunction |
combineWithAnd(Conjuctable formula)
Returns a conjunction of this and the given formula.
|
Disjunction |
combineWithOr(Disjunctable formula) |
RelationalFormula |
complement() |
boolean |
containsQuantifier()
Checks whether this formula contains any quantification.
|
boolean |
equals(java.lang.Object o) |
java.util.Set<FOLAtom> |
getAtoms()
Processes the set of all atoms which appear in this formula
|
FolFormula |
getConclusion() |
java.util.Set<Functor> |
getFunctors() |
java.util.Collection<FolFormula> |
getJustification() |
java.util.Set<? extends Predicate> |
getPredicates()
Processes the set of all predicates which appear in this
formula
|
FolFormula |
getPrerequisite() |
java.util.Set<Variable> |
getQuantifierVariables() |
FolSignature |
getSignature()
Returns the signature of the language of this formula.
|
java.util.Set<Term<?>> |
getTerms() |
<C extends Term<?>> |
getTerms(java.lang.Class<C> cls)
Processes the set containing all terms of type C.
|
java.util.Set<Variable> |
getUnboundVariables() |
Probability |
getUniformProbability() |
int |
hashCode() |
boolean |
isClosed()
Checks whether this formula is closed, i.e.
|
boolean |
isClosed(java.util.Set<Variable> boundVariables)
Checks whether this formula is closed, i.e.
|
boolean |
isLiteral() |
boolean |
isNormal(DefaultTheory dt)
Tests, whether the default is normal
normal ^= a:c/c
|
boolean |
isWellBound()
Checks whether this formula is well-bound, i.e.
|
boolean |
isWellBound(java.util.Set<Variable> boundVariables)
Checks whether this formula is well-bound, i.e.
|
RelationalFormula |
substitute(Term<?> v,
Term<?> t)
Substitutes all occurrences of term "v" in this formula
by term "t" and returns the new formula.
|
java.lang.String |
toString() |
allGroundInstances, allSubstitutions, containsTermsOfType, exchange, getFormula, getPredicateCls, getSatisfactionRatio, isGround, isWellFormed, substitute
private FolFormula pre
private java.util.Collection<FolFormula> jus
private FolFormula conc
public DefaultRule()
public DefaultRule(FolFormula pre, FolFormula jus, FolFormula conc) throws ParserException
ParserException
public DefaultRule(FolFormula pre, java.util.Collection<FolFormula> jus, FolFormula conc) throws ParserException
ParserException
public boolean isNormal(DefaultTheory dt)
public FolFormula getPrerequisite()
public java.util.Collection<FolFormula> getJustification()
public FolFormula getConclusion()
public java.util.Set<? extends Predicate> getPredicates()
SimpleLogicalFormula
public boolean isLiteral()
public java.util.Set<Variable> getQuantifierVariables()
public java.util.Set<Variable> getUnboundVariables()
public boolean containsQuantifier()
QuantifiedFormula
public boolean isWellBound()
QuantifiedFormula
public boolean isWellBound(java.util.Set<Variable> boundVariables)
QuantifiedFormula
boundVariables
- the variables assumed to be bound.public boolean isClosed()
QuantifiedFormula
public boolean isClosed(java.util.Set<Variable> boundVariables)
QuantifiedFormula
boundVariables
- the variables assumed to be bound.public java.util.Set<Term<?>> getTerms()
public <C extends Term<?>> java.util.Set<C> getTerms(java.lang.Class<C> cls)
LogicStructure
cls
- The Class structure containing type information about the
searched termpublic java.util.Set<FOLAtom> getAtoms()
SimpleLogicalFormula
getAtoms
in interface SimpleLogicalFormula
getAtoms
in class RelationalFormula
public java.util.Set<Functor> getFunctors()
getFunctors
in class RelationalFormula
public RelationalFormula substitute(Term<?> v, Term<?> t) throws java.lang.IllegalArgumentException
RelationalFormula
substitute
in interface ComplexLogicalFormula
substitute
in class RelationalFormula
v
- the term to be substituted.t
- the term to substitute.java.lang.IllegalArgumentException
- if "v" and "t" are of different sorts
(NOTE: this exception is only thrown when "v" actually appears in this
formula).public Probability getUniformProbability()
getUniformProbability
in interface ProbabilityAware
getUniformProbability
in class RelationalFormula
public RelationalFormula complement()
complement
in interface Invertable
complement
in class RelationalFormula
public Disjunction combineWithOr(Disjunctable formula)
combineWithOr
in interface Disjunctable
combineWithOr
in class RelationalFormula
formula
- a formula to be combined with OR and this.public Conjunction combineWithAnd(Conjuctable formula)
Conjuctable
combineWithAnd
in interface Conjuctable
combineWithAnd
in class RelationalFormula
formula
- a formula to be combined with AND and this.public FolSignature getSignature()
Formula
getSignature
in interface Formula
getSignature
in class RelationalFormula
public java.lang.String toString()
toString
in class RelationalFormula
public RelationalFormula clone()
SimpleLogicalFormula
clone
in interface ComplexLogicalFormula
clone
in interface SimpleLogicalFormula
clone
in class RelationalFormula
public int hashCode()
hashCode
in interface SimpleLogicalFormula
hashCode
in class java.lang.Object
public boolean equals(java.lang.Object o)
equals
in interface SimpleLogicalFormula
equals
in class java.lang.Object