publication . Preprint . 2020

E-Cyclist: Implementation of an Efficient Validation of FOL ID Cyclic Induction Reasoning (System Description)

Stratulat, Sorin;
Open Access English
  • Published: 03 Feb 2020
  • Publisher: HAL CCSD
  • Country: France
Abstract
Checking the soundness of cyclic induction reasoning for first-order logic with inductive definitions (FOLID) is decidable but the standard checking method is based on an exponential complement operation for Büchi automata. Recently, we introduced a polynomial checking method whose most expensive steps recall the comparisons done with multiset path orderings. We describe the implementation of our method in the Cyclist prover. Referred to as E-Cyclist, it successfully checked all the proofs included in the original distribution of Cyclist. Heuristics have been devised to automatically define from the analysis of the proof derivations the ordering measures that sa...
Subjects
ACM Computing Classification System: TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESTheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
free text keywords: [INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC]

1. The SPIKE theorem prover, 1997-2020. https://github.com/sorinica/spike-prover.

2. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

3. S. Berardi and M. Tatsuta. Classical system of Martin-Lof's inductive definitions is not equivalent to cyclic proofs. Logical Methods in Computer Science, 15(3), 2019.

4. J. Brotherston. Cyclic proofs for first-order logic with inductive definitions. In Proceedings of TABLEAUX-14, volume 3702 of LNAI, pages 78-92. Springer-Verlag, 2005. [OpenAIRE]

5. J. Brotherston. Sequent Calculus Proof Systems for Inductive Definitions. PhD thesis, University of Edinburgh, November 2006. [OpenAIRE]

6. J. Brotherston, N. Gorogiannis, and R. L. Petersen. A generic cyclic theorem prover. In APLAS-10 (10th Asian Symposium on Programming Languages and Systems), volume 7705 of LNCS, pages 350-367. Springer, 2012.

7. J. Brotherston and A. Simpson. Sequent calculi for induction and infinite descent. Journal of Logic and Computation, 21(6):1177-1216, 2011.

8. G. Gentzen. Untersuchungen über das logische Schließen. I. Mathematische Zeitschrift, 39:176-210, 1935.

9. M. Michel. Complementation is more difficult with automata on infinite words. Technical report, CNET, 1988.

10. S. Stratulat. Cyclic proofs with ordering constraints. In R. A. Schmidt and C. Nalon, editors, TABLEAUX 2017 (26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods), volume 10501 of LNAI, pages 311-327. Springer, 2017. [OpenAIRE]

11. S. Stratulat. Mechanically certifying formula-based Noetherian induction reasoning. Journal of Symbolic Computation, 80, Part 1:209-249, 2017. [OpenAIRE]

12. S. Stratulat. Validating back-links of FOLID cyclic pre-proofs. In S. Berardi and S. van Bakel, editors, CL&C'18 (Seventh International Workshop on Classical Logic and Computation), number 281 in EPTCS, pages 39-53, 2018. [OpenAIRE]

13. The Coq development team. The Coq Reference Manual. INRIA, 2020.

Abstract
Checking the soundness of cyclic induction reasoning for first-order logic with inductive definitions (FOLID) is decidable but the standard checking method is based on an exponential complement operation for Büchi automata. Recently, we introduced a polynomial checking method whose most expensive steps recall the comparisons done with multiset path orderings. We describe the implementation of our method in the Cyclist prover. Referred to as E-Cyclist, it successfully checked all the proofs included in the original distribution of Cyclist. Heuristics have been devised to automatically define from the analysis of the proof derivations the ordering measures that sa...
Subjects
ACM Computing Classification System: TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESTheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
free text keywords: [INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC]

1. The SPIKE theorem prover, 1997-2020. https://github.com/sorinica/spike-prover.

2. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.

3. S. Berardi and M. Tatsuta. Classical system of Martin-Lof's inductive definitions is not equivalent to cyclic proofs. Logical Methods in Computer Science, 15(3), 2019.

4. J. Brotherston. Cyclic proofs for first-order logic with inductive definitions. In Proceedings of TABLEAUX-14, volume 3702 of LNAI, pages 78-92. Springer-Verlag, 2005. [OpenAIRE]

5. J. Brotherston. Sequent Calculus Proof Systems for Inductive Definitions. PhD thesis, University of Edinburgh, November 2006. [OpenAIRE]

6. J. Brotherston, N. Gorogiannis, and R. L. Petersen. A generic cyclic theorem prover. In APLAS-10 (10th Asian Symposium on Programming Languages and Systems), volume 7705 of LNCS, pages 350-367. Springer, 2012.

7. J. Brotherston and A. Simpson. Sequent calculi for induction and infinite descent. Journal of Logic and Computation, 21(6):1177-1216, 2011.

8. G. Gentzen. Untersuchungen über das logische Schließen. I. Mathematische Zeitschrift, 39:176-210, 1935.

9. M. Michel. Complementation is more difficult with automata on infinite words. Technical report, CNET, 1988.

10. S. Stratulat. Cyclic proofs with ordering constraints. In R. A. Schmidt and C. Nalon, editors, TABLEAUX 2017 (26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods), volume 10501 of LNAI, pages 311-327. Springer, 2017. [OpenAIRE]

11. S. Stratulat. Mechanically certifying formula-based Noetherian induction reasoning. Journal of Symbolic Computation, 80, Part 1:209-249, 2017. [OpenAIRE]

12. S. Stratulat. Validating back-links of FOLID cyclic pre-proofs. In S. Berardi and S. van Bakel, editors, CL&C'18 (Seventh International Workshop on Classical Logic and Computation), number 281 in EPTCS, pages 39-53, 2018. [OpenAIRE]

13. The Coq development team. The Coq Reference Manual. INRIA, 2020.

Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue