Implementation of two reasoning models with Horn clauses and Resolution.
The program is reading clauses from a knowledge base to check whether the resolution is right. This is accomplished by comparing a clause with its opposite.
Dictionary format :
- NOT operator is presented as "-"
- AND operator is presented as the change line “\n”
- OR operator is presented as space " "
- CNFClause : Arraylist of CNF subclauses (with the same parent) linked to the "AND" operator.
- Literal : Contains the Literal of a clause, checking if it is negative or not.
- MainResolution : Performs the resolution algorithm for the provided files (knowledge base and the negative clause) via PL_Analysis method. Finally, it shows whether the negative clause is true or false.
- SubClause : Contains HashSet Literals for each sub-clause of a CNF clause.
- CNFUtils : Reads data from the given files. (Common class for both propositional models)
A Knowledge Base which is formatted as seen below:
Each line corresponds to a Horn clause ("\n").
- AND operator is presented as " "
- "=>" (conclusion) operator is presented as “=>”
- ClauseHorn: Arraylist of Horn clauses symbols.
- KB( KnowledgeBase): In this class we store the suggestions for the knowledge base. Storing Horn clauses into two ArrayLists. Inside the first ArrayList we store the symbols that were only in the knowledge base (facts)
and inside the second Horn clause ArrayList we insert the clauses that are excluded from the facts.
- MainHorn : Saves the current knowledge base and the set of symbols which the user gives as input to check which of the components are valid (or q! to exit). Afterwards the forward chaining reasoning algorithm is executed, where true is returned
or false, depending on whether the symbol is located or not.
- CNFUtils : Reads data from the given files (Common class for both propositional models).
Contains the necessary text files for the knowledge base and the clause we want, which are also used as examples.