The students can work with propositional logic, and first order logic. It also gives the tree form of the formula. The program can put the formulas in normal form, CNF, DNF, and Skolam normal form. There is an implementation of the unification algorithm.
Resolution is implemented for propositional logic and first order logic.
The main objective of the software is to be didactical. So the students can see how to solve exercices step by step, forwards and backwards. IloTutorCP0 is the application for propositional logic. IloTutorCP1 is the application for first order logic. Exemples contains some examples to try out.