Document Open Access Logo

Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent

Authors Liron Cohen, Reuben N. S. Rowe

PDF
Thumbnail PDF

File

LIPIcs.CSL.2018.17.pdf
  • Filesize: 0.5 MB
  • 16 pages

Document Identifiers

Author Details

Liron Cohen
  • Dept. of Computer Science, Cornell University, NY, USA
Reuben N. S. Rowe
  • School of Computing, University of Kent, Canterbury, UK

Funding

  • Cohen, Liron: Supported by Fulbright Post-doctoral Scholar program, Weizmann Institute of Science National Postdoctoral Award program for Advancing Women in Science, and Eric and Wendy Schmidt Postdoctoral Award program for Women in Mathematical and Computing Sciences.
  • Rowe, Reuben N. S.: Supported by EPSRC Grant No. EP/N028759/1.

Cite As Get BibTex

Liron Cohen and Reuben N. S. Rowe. Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 17:1-17:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CSL.2018.17

Abstract

Transitive closure logic is a known extension of first-order logic obtained by introducing a transitive closure operator. While other extensions of first-order logic with inductive definitions are a priori parametrized by a set of inductive definitions, the addition of the transitive closure operator uniformly captures all finitary inductive definitions. In this paper we present an infinitary proof system for transitive closure logic which is an infinite descent-style counterpart to the existing (explicit induction) proof system for the logic. We show that, as for similar systems for first-order logic with inductive definitions, our infinitary system is complete for the standard semantics and subsumes the explicit system. Moreover, the uniformity of the transitive closure operator allows semantically meaningful complete restrictions to be defined using simple syntactic criteria. Consequently, the restriction to regular infinitary (i.e. cyclic) proofs provides the basis for an effective system for automating inductive reasoning.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Automated reasoning
Keywords
  • Induction
  • Transitive Closure
  • Infinitary Proof Systems
  • Cyclic Proof Systems
  • Soundness
  • Completeness
  • Standard Semantics
  • Henkin Semantics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Arnon Avron. Transitive Closure and the Mechanization of Mathematics. In F. D. Kamareddine, editor, Thirty Five Years of Automating Mathematics, volume 28 of Applied Logic Series, pages 149-171. Springer, Netherlands, 2003. URL: http://dx.doi.org/10.1007/978-94-017-0253-9_7.
  2. Stefano Berardi and Makoto Tatsuta. Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System. In Proceedings of FOSSACS, Uppsala, Sweden, April 22-29, 2017, pages 301-317, Berlin, Heidelberg, 2017. Springer. URL: http://dx.doi.org/10.1007/978-3-662-54458-7_18.
  3. Stefano Berardi and Makoto Tatsuta. Equivalence of Inductive Definitions and Cyclic Proofs Under Arithmetic. In Proceedings of LICS, Reykjavik, Iceland, June 20-23, 2017, pages 1-12, 2017. URL: http://dx.doi.org/10.1109/LICS.2017.8005114.
  4. James Brotherston. Formalised Inductive Reasoning in the Logic of Bunched Implications. In Proceedings of SAS, Kongens Lyngby, Denmark, August 22-24, 2007, pages 87-103, 2007. URL: http://dx.doi.org/10.1007/978-3-540-74061-2_6.
  5. James Brotherston, Richard Bornat, and Cristiano Calcagno. Cyclic Proofs of Program Termination in Separation Logic. In Proceedings of POPL, San Francisco, California, USA, January 7-12, 2008, pages 101-112, 2008. URL: http://dx.doi.org/10.1145/1328438.1328453.
  6. James Brotherston and Alex Simpson. Sequent Calculi for Induction and Infinite Descent. Journal of Logic and Computation, 21(6):1177-1216, 2010. Google Scholar
  7. Samuel R. Buss. Handbook of Proof Theory. Studies in Logic and the Foundations of Mathematics. Elsevier Science, 1998. Google Scholar
  8. Liron Cohen. Ancestral Logic and Equivalent Systems. Master’s thesis, Tel-Aviv University, Israel, 2010. Google Scholar
  9. Liron Cohen. Completeness for Ancestral Logic via a Computationally-Meaningful Semantics. In Proceedings of TABLEAUX, Brasília, Brazil, September 25-28, 2017, pages 247-260, 2017. URL: http://dx.doi.org/10.1007/978-3-319-66902-1_15.
  10. Liron Cohen and Arnon Avron. Ancestral Logic: A Proof Theoretical Study. In U. Kohlenbach, editor, Logic, Language, Information, and Computation, volume 8652 of Lecture Notes in Computer Science, pages 137-151. Springer, 2014. Google Scholar
  11. Liron Cohen and Arnon Avron. The Middle Ground-Ancestral Logic. Synthese, pages 1-23, 2015. Google Scholar
  12. Liron Cohen and Reuben N. S. Rowe. Infinitary and Cyclic Proof Systems for Transitive Closure Logic. CoRR, abs/1802.00756, 2018. URL: http://arxiv.org/abs/1802.00756.
  13. Stephen A. Cook and Robert A. Reckhow. The Relative Efficiency of Propositional Proof Systems. The Journal of Symbolic Logic, 44(1):36-50, 1979. Google Scholar
  14. Bruno Courcelle. Fundamental Properties of Infinite Trees. Theor. Comput. Sci., 25:95-169, 1983. URL: http://dx.doi.org/10.1016/0304-3975(83)90059-2.
  15. Anupam Das and Damien Pous. A Cut-Free Cyclic Proof System for Kleene Algebra. In Proceedings of TABLEAUX, Brasília, Brazil, September 25-28, 2017, pages 261-277, 2017. URL: http://dx.doi.org/10.1007/978-3-319-66902-1_16.
  16. Gerhard Gentzen. Untersuchungen über das Logische Schließen. I. Mathematische Zeitschrift, 39(1):176-210, 1935. URL: http://dx.doi.org/10.1007/BF01201353.
  17. Jean-Yves Girard. Proof Theory and Logical Complexity, volume 1. Humanities Press, 1987. Google Scholar
  18. Leon Henkin. Completeness in the Theory of Types. Journal of Symbolic Logic, 15(2):81-91, 1950. Google Scholar
  19. Ryo Kashima and Keishi Okamoto. General Models and Completeness of First-order Modal μ-calculus. Journal of Logic and Computation, 18(4):497-507, 2008. Google Scholar
  20. Laurie Kirby and Jeff Paris. Accessible Independence Results for Peano Arithmetic. Bulletin of the London Mathematical Society, 14(4):285-293, 1982. URL: http://dx.doi.org/10.1112/blms/14.4.285.
  21. Per Martin-Löf. Hauptsatz for the Intuitionistic Theory of Iterated Inductive Definitions. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, volume 63 of Studies in Logic and the Foundations of Mathematics, pages 179-216. Elsevier, 1971. URL: http://dx.doi.org/10.1016/S0049-237X(08)70847-4.
  22. Per Martin-Löf and Giovanni Sambin. Intuitionistic Type Theory, volume 9. Bibliopolis Napoli, 1984. Google Scholar
  23. Reuben N. S. Rowe and James Brotherston. Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic. In Proceedings of CPP, Paris, France, January 16-17, 2017, pages 53-65, 2017. URL: http://dx.doi.org/10.1145/3018610.3018623.
  24. Luigi Santocanale. A Calculus of Circular Proofs and Its Categorical Semantics. In Proceedings of FOSSACS, Grenoble, France, April 8-12, 2002, pages 357-371. Springer Berlin Heidelberg, 2002. URL: http://dx.doi.org/10.1007/3-540-45931-6_25.
  25. Kurt Schütte. Beweistheoretische Erfassung der unendlichen Induktion in der Zahlentheorie. Mathematische Annalen, 122:369-389, 1950/51. Google Scholar
  26. Alex Simpson. Cyclic Arithmetic Is Equivalent to Peano Arithmetic. In Proceedings of FOSSACS, Uppsala, Sweden, April 22-29, 2017, pages 283-300, 2017. URL: http://dx.doi.org/10.1007/978-3-662-54458-7_17.
  27. Christoph Sprenger and Mads Dam. On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the μ-Calculus. In Proceedings of FOSSACS, Warsaw, Poland, April 7-11, 2003, pages 425-440. Springer Berlin Heidelberg, 2003. URL: http://dx.doi.org/10.1007/3-540-36576-1_27.
  28. Gaisi Takeuti. Proof Theory. Courier Dover Publications, 1987. Google Scholar
  29. Gadi Tellez and James Brotherston. Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof. In Proceedings of CADE, Gothenburg, Sweden, August 6-11, 2017, pages 491-508, 2017. URL: http://dx.doi.org/10.1007/978-3-319-63046-5_30.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact