Abstract
We describe the design and implementation of an automated theorem prover realising a fully general notion of cyclic proof. Our tool, called \(\textsc{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. \(\textsc{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 \(\textsc{Cyclist}\) offers significant potential as a future platform for inductive theorem proving.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Cyclist framework download, http://www.cs.ucl.ac.uk/staff/ngorogia/
Avenhaus, J., Kühler, U., Schmidt-Samoa, T., Wirth, C.-P.: How to Prove Inductive Theorems? QuodLibet! In: Baader, F. (ed.) CADE-19. LNCS (LNAI), vol. 2741, pp. 328–333. Springer, Heidelberg (2003)
Berdine, J., Cook, B., Distefano, D., O’Hearn, P.W.: Automatic Termination Proofs for Programs with Shape-Shifting Heaps. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 386–400. Springer, Heidelberg (2006)
Brotherston, J.: Cyclic Proofs for First-Order Logic with Inductive Definitions. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol. 3702, pp. 78–92. Springer, Heidelberg (2005)
Brotherston, J.: Sequent Calculus Proof Systems for Inductive Definitions. Ph.D. thesis, University of Edinburgh (November 2006)
Brotherston, J.: Formalised Inductive Reasoning in the Logic of Bunched Implications. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 87–103. Springer, Heidelberg (2007)
Brotherston, J., Bornat, R., Calcagno, C.: Cyclic proofs of program termination in separation logic. In: POPL-35, pp. 101–112. ACM (2008)
Brotherston, J., Distefano, D., Petersen, R.L.: Automated Cyclic Entailment Proofs in Separation Logic. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 131–146. Springer, Heidelberg (2011)
Brotherston, J., Simpson, A.: Sequent calculi for induction and infinite descent. Journal of Logic and Computation 21(6), 1177–1216 (2011)
Bundy, A.: The automation of proof by mathematical induction. In: Handbook of Automated Reasoning, vol. I, ch. 13, pp. 845–911. Elsevier Science (2001)
Couvreur, J.-M.: On-the-fly Verification of Linear Temporal Logic. In: Wing, J., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 253–271. Springer, Heidelberg (1999)
Dixon, L., Fleuriot, J.: IsaPlanner: A Prototype Proof Planner in Isabelle. In: Baader, F. (ed.) CADE-19. LNCS (LNAI), vol. 2741, pp. 279–283. Springer, Heidelberg (2003)
Duret-Lutz, A., Poitrenaud, D.: Spot: An extensible model checking library using transition-based generalized Büchi automata. In: MASCOTS, pp. 76–83 (2004)
Fogarty, S., Vardi, M.Y.: Büchi Complementation and Size-Change Termination. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 16–30. Springer, Heidelberg (2009)
Friedgut, E., Kupferman, O., Vardi, M.Y.: Büchi Complementation Made Tighter. In: Wang, F. (ed.) ATVA 2004. LNCS, vol. 3299, pp. 64–78. Springer, Heidelberg (2004)
Johansson, M., Dixon, L., Bundy, A.: Conjecture synthesis for inductive theories. Journal of Automated Reasoning 47(3) (October 2011)
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer (2000)
Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL-28, pp. 81–92. ACM (2001)
Nguyen, H.H., Chin, W.N.: Enhancing Program Verification with Lemmas. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 355–369. Springer, Heidelberg (2008)
Schöpp, U., Simpson, A.: Verifying Temporal Properties Using Explicit Approximants: Completeness for Context-free Processes. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 372–386. Springer, Heidelberg (2002)
Sprenger, C., Dam, M.: A note on global induction mechanisms in a μ-calculus with explicit approximations. Theor. Informatics and Applications 37, 365–399 (2003)
Sprenger, C., Dam, M.: On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the μ-Calculus. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 425–440. Springer, Heidelberg (2003)
Stirling, C., Walker, D.: Local model checking in the modal μ-calculus. Theoretical Computer Science 89, 161–177 (1991)
Wirth, C.P.: Descente infinie + Deduction. Logic J. of the IGPL 12(1), 1–96 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brotherston, J., Gorogiannis, N., Petersen, R.L. (2012). A Generic Cyclic Theorem Prover. In: Jhala, R., Igarashi, A. (eds) Programming Languages and Systems. APLAS 2012. Lecture Notes in Computer Science, vol 7705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35182-2_25
Download citation
DOI: https://doi.org/10.1007/978-3-642-35182-2_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35181-5
Online ISBN: 978-3-642-35182-2
eBook Packages: Computer ScienceComputer Science (R0)