A generic cyclic theorem prover

We describe the design and implementation of an automated theorem prover realising a fully general notion of cyclic proof. Our tool, called CYCLIST, is able to construct proofs obeying a very general cycle scheme in which leaves may be linked to any other matching node in the proof, and to verify the general, global infinitary condition on such proof objects ensuring their soundness. CYCLIST is based on a new, generic theory of cyclic proofs that can be instantiated to a wide variety of logics. We have developed three such concrete instantiations, based on: (a) first-order logic with inductive definitions; (b) entailments of pure separation logic; and (c) Hoare-style termination proofs for pointer programs. Experiments run on these instantiations indicate that CYCLIST offers significant potential as a future platform for inductive theorem proving. © Springer-Verlag Berlin Heidelberg 2012