We read the knowledge base from the knowledgebase file that has the form: A1 AND A2 AND ... AND AN => H1 A1 AND A2 AND ... AND AM => H2
INFO Each line is a fixed Horn clause, where Ai are atomic types consisting of Premises and Hi are the Heads.
There are spaces before and after every AND but not before and after =>. The term that we want to be proved can be atomic and is given by the keypad.
- Atomic: This class implements an atomic type. Atomic types can either be an equation with the form of t1 = t2, where t1 and t2 are either terms or relationship symbol (predicate). The Booleans isEq and isRelSymb are to determine which of the two forms is the atomic mode.
- DefClauseKB: This class implements a knowledge base, a CNF that is consisted of definite horn clauses
- DefiniteClause: This class implements a definite horn clause
- Main: In the main class, we are using the folfcAsk algorithm.
- Subst: We have implemented an substitution in the forn {variable / term}
- Term: Implementing a term. We use the code to identify whether a term is a 1-variable, 2-constant, 3-relationship symbol.
- Unifier: We implement the Algorithm of Unification.