Proof Search for the First-Order Connection Calculus in Maude

Abstract

This paper develops a rewriting logic specification of the connection method for first-order logic, implemented in Maude. The connection method is a goal-directed proof procedure that requires a careful control over clause copies. The specification separates the inference rule layer from the rule application layer, and implements the latter at Maude's meta-level. This allows us to develop and compare different strategies for proof search.

Publication
In Proc. 7th Intl. Workshop on Rewriting Logic and its Applications (WRLA’08). Electronic Notes in Theoretical Computer Science 238:173-188, 2009. © Elsevier.
Date