Skip to main content
SpringerLink
Log in

Proof Search and Proof Check for Equational and Inductive Theorems

  • Conference paper
Book cover Automated Deduction – CADE-19 (CADE 2003)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2741))

Included in the following conference series:

Abstract

This paper presents on-going researches on theoretical and practical issues of combining rewriting based automated theorem proving and user-guided proof development, with the strong constraint of safe cooperation of both. In practice, we instantiate the theoretical study on the Coq proof assistant and the ELAN rewriting based system, focusing first on equational and then on inductive proofs. Different concepts, especially rewriting calculus and deduction modulo, contribute to define and to relate proof search, proof representation and proof check.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ahrendt, W., Beckert, B., Hähnle, R., Menzel, W., Reil, W., Schellhorn, G., Schmitt, P.: Integrating automated and interactive theorem proving. In: Bibel, W., Schmitt, P. (eds.) Automated - A Basis for Applications, vol. 1. Kluwer Academic Publishers, Dordrecht (1998)

    Google Scholar 

  2. Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J.: Explicit substitutions. In: ACM (ed.) Conf. Rec. 17th Symp. POPL, pp. 31–46 (1990)

    Google Scholar 

  3. Appel, A.W., Felty, A.P.: A semantic model of types and machine instructions for proof-carrying code. In: Proc. of 27th POPL, pp. 243–253 (January 2000)

    Google Scholar 

  4. Appel, A.W.: Foundational proof-carrying code. In: Proc. 16th LICS, pp. 247–258 (June 2001)

    Google Scholar 

  5. Barendregt, H., Barendsen, E.: Autarkic computations in formal proofs. Journal of Automated Reasoning 28(3), 321–336 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  6. Bezem, M., Hendriks, D., de Nivelle, H.: Automated proof construction in type theory using resolution. Journal of Automated Reasoning 29(3-4), 253–275 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  7. Borovansky, P., Kirchner, C., Kirchner, H., Moreau, P.-E.: ELAN from a rewriting logic point of view. Theoretical Computer Science (285), 155–185 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  8. Bouhoula, A., Kounalis, E., Rusinowitch, M.: Spike: An automatic theorem prover. In: Voronkov, A. (ed.) LPAR 1992. LNCS (LNAI), vol. 624, pp. 460–462. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  9. Boutin, S.: Using reflection to build efficient and certified decision procedures. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol. 1281, pp. 515–529. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  10. Boulton, R., Slind, K., Bundy, A., Gordon, M.: An interface between clam and HOL. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 87–104. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  11. Coquand, T., Huet, G.: The Calculus of Constructions. Information and Computation 76 (1988)

    Google Scholar 

  12. Curien, P.-L., Hardin, T., Lévy, J.-J.: Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM 43(2), 362–397 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  13. Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic 5, 56–68 (1940)

    Article  MATH  MathSciNet  Google Scholar 

  14. Cirstea, H.: Calcul de réécriture: fondements et applications. Thèse de Doctorat d’Université, Université Henri Poincaré - Nancy 1 (October 2000)

    Google Scholar 

  15. Cirstea, H., Kirchner, C.: The rewriting calculus — Part I and II. Logic Journal of the Interest Group in Pure and Applied Logics 9(3), 427–498 (2001)

    MathSciNet  Google Scholar 

  16. Deplagne, E.: Système de preuve modulo récurrence. Thèse de doctorat, Université Nancy 1 (November 2002)

    Google Scholar 

  17. Dowek, G., Hardin, T., Kirchner, C.: HOL-λσ an intentional first-order expression of higher-order logic. Mathematical Structures in Computer Science 11(1), 21–45 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  18. Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Journal of Automated Reasoning (2003) (to appear), See also ftp://ftp.inria.fr/INRIA/publication/RR/RR-3400.ps.gz

  19. Deplagne, E., Kirchner, C.: Induction as deduction modulo. Research report, Loria (2003) (in preparation)

    Google Scholar 

  20. Dowek, G.: La part du Calcul. Mémoire d’habilitation, Université de Paris 7 (1999)

    Google Scholar 

  21. Goubault-Larrecq, J.: Well-founded recursive relations. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 484–497. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  22. Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge, UK (1995), Available at http://www.cl.cam.ac.uk/users/jrh/papers/reflect.dvi.gz+

  23. Harrison, J., Théry, L.: A sceptic’s approach to combining hoal and mapple. Journal of Automated Reasoning 21, 279–294 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  24. Hurd, J.: Integrating gandalf and HOL. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 311–321. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  25. Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM Journal of Computing 15(4), 1155–1194 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  26. Joyce, J., Seger, C.: The HOL-Voss system: Model-checking inside a general-purpose theorem-prover. In: Joyce, J.J., Seger, C.-J.H. (eds.) HUG 1993. LNCS, vol. 780, pp. 185–198. Springer, Heidelberg (1994)

    Google Scholar 

  27. Kirchner, H., Moreau, P.-E.: Promoting rewriting to a programming language: A compiler for non-deterministic rewrite programs in associativecommutative theories. Journal of Functional Programming 11(2), 207–251 (2001); Report LORIA A01-R-007

    MATH  MathSciNet  Google Scholar 

  28. Kapur, D., Zhang, H.: An overview of rewrite rule laboratory (rrl). J. Computer and Mathematics with Applications 29(2), 91–114 (1995)

    Article  MathSciNet  Google Scholar 

  29. Leclerc, F.: Termination proof of term rewriting systems with the multiset path ordering: A complete development in the system coq. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 312–327. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  30. Necula, G.C.: Proof-carrying code. In: Proc. of 24th POPL, pp. 106–119 (January 1997)

    Google Scholar 

  31. Nguyen, Q.-H.: Calcul de réécriture et automatisation du raisonnement dans les assistants de preuve. Thèse de Doctorat d’Université, Université Henri Poincaré - Nancy 1 (October 2002)

    Google Scholar 

  32. Nguyen, Q.-H.: A constructive decision procedure for equalities modulo AC. In: Ringeissen, C., Tinelli, C., Treinen, R., Verma, R. (eds.) Proc. of 18th UNIF, pp. 59–63 (2002)

    Google Scholar 

  33. Nguyen, Q.-H., Kirchner, C., Kirchner, H.: External rewriting for skeptical proof assistants. Journal of Automated Reasoning 29(3-4), 309–336 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  34. Necula, G., Lee, P.: Efficient representation and validation of logical proofs. In: Proc. LICS 1998, pp. 93–104 (June 1998)

    Google Scholar 

  35. Paulson, L.: A Generic Tableau Prover and its Integration with Isabelle. Journal of Universal Computer Science 5(3), 73–87 (1999)

    MATH  MathSciNet  Google Scholar 

  36. Paulin-Mohring, C.: Inductive definitions in the system Coq: Rules and properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 328–345. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  37. Peterson, G., Stickel, M.E.: Complete sets of reductions for some equational theories. Journal of the ACM 28, 233–264 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  38. Pfenning, F., Schürmann, C.: System description: Twelf - a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS, vol. 1632, pp. 202–206. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  39. Rushby, J.: Integrated formal verification: Using model checking with automated abstraction, invariant generation, and theorem proving. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 311–321. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  40. Stump, A., Dill, D.L.: Faster proof checking in the Edinburgh Logical Framework. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 391–406. Springer, Heidelberg (2002)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LORIA-INRIA-CNRS, BP 239, F-54506, Vandœuvre-lès-Nancy Cedex

    Eric Deplagne, Claude Kirchner, Hélène Kirchner & Quang Huy Nguyen

Authors
  1. Eric Deplagne
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Claude Kirchner
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Hélène Kirchner
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Quang Huy Nguyen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Theoretical Computer Science, TU Dresden, Germany

    Franz Baader

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Deplagne, E., Kirchner, C., Kirchner, H., Nguyen, Q.H. (2003). Proof Search and Proof Check for Equational and Inductive Theorems. In: Baader, F. (eds) Automated Deduction – CADE-19. CADE 2003. Lecture Notes in Computer Science(), vol 2741. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45085-6_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-45085-6_26

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40559-7

  • Online ISBN: 978-3-540-45085-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation