A web-based education system for predicate logic

In this paper, we present a web-based system teaching predicate logic as a knowledge representation and reasoning language. The system is adaptable in the sense that it allows the students to choose their own way of using it. Students can evaluate themselves, by selecting the complexity and the difficulty level of the exercises. Another interesting point of the system is its open exercising facility, by which the students can try any conversion of a FOPC formula to Clause Form. This is achieved by calling LISP code, which is part of an automated theorem prover. Incorporation of LISP code into the hypermedia application was an interesting implementation problem. An initial evaluation of the system showed encouraging results as far as its usability and learning are concerned.