Package ai.krr.fol

Interface Summary
Substitution A Substitution maps a set of Variables to a set of Terms.
TheoremProver This interface represents a theorem prover for first-order logic.
 

Class Summary
Atom An Atom is one of the most basic building blocks for a Sentence.
BinaryConnectedSentence This class represents a Sentence that consists of a Connective that connects two sub-Sentences.
Clause  
ConnectedSentence This class represents a Sentence that consists of a Connective that connects a number of (at least two) sub-Sentences.
Constant The most basic Term is a Constant that is represented by a Symbol.
FunctionTerm This class allows to build structured Terms that consist of a function symbol and a number of arguments.
HerbrandGenerator  
HerbrandGenerator.HerbrandUniverse  
Instantiation An Instantiation maps a set of Variables to a set of Terms.
Interpretation An Interpretation over a domain D in first-order logic is an assignment of:
KifKnowledgeBaseAdaptor  
KifSentenceAdaptor This class is an adaptor between the ai.krr.propositions.Sentence class that can be used as an internal representation for reasoning and its external form as defined by the KIF syntax as described below.
KifSentenceAdaptor.VariableStack  
KnowledgeBase A KnowledgeBase is effectively a set of Sentences believed to be true.
Literal A Literal is one of the most basic building blocks for a Sentence.
NegatedSentence A NegatedSentence is the simplest kind of complex Sentence.
QuantifiedSentence  
Sentence A Sentence is usually used in logic to represent a proposition that is either true or false.
Term A Term represents an object in a conceptualisation of some domain.
TruthValue A TruthValue is one of the most basic building blocks for a Sentence.
Variable This class implements symbolic variables in Java.
VariableRenaming A VariableRenaming maps a set of Variables to a set of Variables.
XfolSentenceAdaptor This class is an adaptor between the ai.krr.propositions.Sentence class that can be used as an internal representation for reasoning and its external form in an XML Syntax.
 

Enum Summary
ConnectedSentence.Connective This enumeration defines the possible connectives that can connect the sub-Sentences.
QuantifiedSentence.Quantifier This enumeration defines the possible quantifiers that bind variables in the content Sentence.