this project implements a First-order Logic resolution program. That includes a Parser, CNF and Skolemization conversions, and Unification.
- to run the unit tests use
julia tests.jl
- to run the examples use
julia examples\barber.jl
andjulia examples\hound_problem.jl
- to use indivisual functions, make sure to
include("hw2.jl")
hw2.jl
: all modules and libraries importedglobals.jl
: global variables such as unique variable names counterstructs.jl
: holds the definitions of all structs (Clause, Knowledge Base, Quantifier, Signature), as well as the verifyTheory() testParser.jl
: parses a string and returns objects of Clauses and/or QuantifiersClause.jl
andKnowledgeBase.jl
: both contain Clauses or KB specific functions, such as Equal and Copyidentifiers.jl
: contains the functions used to identify different types of objects/stringsoperations.jl
: contains functions used for Boolean algebra and operationsprinters.jl
: holds different printing functions for different object types and functionsCNF.jl
: converts a Clause to CNF formskolemization.jl
: converts a CNF clause to a Skolem formMGU.jl
: returns general unifiers for two clausesresolution.jl
: uses all above to resolve a query given a KB
- a Clause instance is basically a Literal but it was too late to change the name ;/
- a KnowledgeBase holds an array of array of Clauses. A Knowledgebase represents {} in FOL (conjunctions), and the arrays of Clauses (Literals) represent [] (disjunctions). So a KB is a conjunction of disjunctions.
- a Clause has an operator, and a list of arguments. A Clause can be
- variable: lowercase operator and zero arguments
- functions: lowercase operator with arguments
- constant: uppercase operator with no arguments
- relation: uppercase operator with arguments
- symbol: is any of the above
- a Quantifier holds an operator, variable, and a Clause
- String statements must be passed to lexer() to parse and separate the different components and combine by precedence. Then passed to toClause() to convert to a Clause object.
- Skolemization here does two things, get rid of quantifiers properly and standarize variables such that every new variable we need is a unique one in the KB
- the current resolution algorithm prints redundant steps
- the unifier shows redundant substituions (x->x or C->C) but they do not affect the algorithm
- Q1:
Parser.jl
andstructs.jl
- Q2:
CNF.jl
andskolemization.jl
- Q3:
MGU.jl
- Q4:
resolution.jl
andexamples\barber.jl
most examples and tests are inspired from