Equality Preprocessing in Connection Calculi (EPICC)

Equality is a fundamental concept in first-order reasoning, yet for connection based proof methods a notoriously challenging one to handle efficiently. While paramodulation is a popular technique for resolution and related calculi, there is no single practical successful solution for connection based approaches. This thesis presents an extensible system for equality preprocessing in connection calculi that can be used as a tool in reducing the search space of problems that contain equality. A number of preprocessing rules are described and subsequently used in the implementation of a preprocessing system (EPICC) written in the Clojure programming language. The leanCoP core connection prover is extended to use the EPICC system for handling equality and it is shown that the resulting system performs better than the current equality handling approach used by leanCoP