Implementing a fragment of first-order logic
Abstract
Coherent logic (CL) is a fragment of full first-order logic, but it is as expressive as the whole of first-order logic (FOL).
Thus, a calculus for this fragment can, together with a translation, provide an efficient proof procedure for FOL. In fact,
many interesting problems can be formalized in CL without any translation. Moreover, proofs in CL do not require the process
known as skolemization. This makes CL calculi well suited for proof assistants as opposed to provers: The formalism preserves
the structure of the problem and therefore one's intuition about it. A calculus for CL called "CL hypertableaux"
has been proposed (see the references), but it has never been implemented, and it is not known whether this calculus will
perform well in practice. The two rules of the calculus are pretty simple to implement, but a naive implementation is likely
to be rather slow. The project would involve implementing the calculus and then investigating how its performance can be optimized.
There are several possible points of optimization that could be interesting to investigate: 1) Efficient data structures
for the clause set, which can represent instances efficiently, and find rule applications efficiently (RETE algorithm, see
references).. 2) Efficient data structures for terms and unifiers (there are no function symbols, so potentially this can
be done very fast) 3) Strategies for rule application (one is discussed in the Master's thesis given in the references, others
may be possible). References: 1) Master's thesis: http://www.duo.uio.no/sok/work.html?WORKID=91821⟨=en 2) Two-page
abstract in Proc of comlab student conference 3) RETE algorithm: http://en.wikipedia.org/wiki/Rete_algorithm
