research-article

Theorem Proving Modulo

Authors:

Thérèse Hardin,

Claude KirchnerAuthors Info & Claims

Journal of Automated Reasoning, Volume 31, Issue 1

Pages 33 - 72

https://doi.org/10.1023/A:1027357912519

Published: 01 September 2003 Publication History

Abstract

Deduction modulo is a way to remove computational arguments from proofs by reasoning modulo a congruence on propositions. Such a technique, issued from automated theorem proving, is of general interest because it permits one to separate computations and deductions in a clean way. The first contribution of this paper is to define a sequent calculus modulo that gives a proof-theoretic account of the combination of computations and deductions. The congruence on propositions is handled through rewrite rules and equational axioms. Rewrite rules apply to terms but also directly to atomic propositions.

The second contribution is to give a complete proof search method, called extended narrowing and resolution (ENAR), for theorem proving modulo such congruences. The completeness of this method is proved with respect to provability in sequent calculus modulo.

An important application is that higher-order logic can be presented as a theory in deduction modulo. Applying the ENAR method to this presentation of higher-order logic subsumes full higher-order resolution.

References

[1]

Abadi M., Cardelli L., Curien P.-L., and Lévy J.-J. Explicit substitutions J. Funct. Programming 1991 1 4 375-416

[2]

Andrews P. B. Resolution in type theory J. Symbolic Logic 1971 36 414-432

[3]

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

[4]

Bachmair L. Proof methods for equational theories 1987 Urbana-Champaign, IL University of Illinois

[5]

Bachmair L., Ganzinger H., Lynch C., and Snyder W. Basic paramodulation Inform. and Comput. 1995 121 2 172-192

[6]

Barendregt H. and Barendsen E. Autartik computations in formal proofs J. Automated Reasoning 2002 28 3 321-336

[7]

Bürckert H.-J. Stickel M. E. A resolution principle for clauses with constraints Proceedings 10th International Conference on Automated Deduction, Kaiserslautern (Germany) 1990 New York Springer-Verlag 178-192

[8]

Bürckert, H.-J.: A Resolution Principle for a Logic with Restricted Quantifiers, Lecture Notes in Artificial Intelligence 568, Springer-Verlag, 1991.

[9]

Curien P.-L., Hardin T., and Lévy J.-J. Confluence properties of weak and strong calculi of explicit substitutions J. ACM 1996 43 2 362-397

[10]

Degtyarev, A. and Voronkov, A.: Equality reasoning in sequent-based calculi, in A. Robinson and A. Voronkov (eds.), Handbook of Automated Reasoning, Vol. I, Elsevier, 2001, Chapt. 10, pp. 611-706.

[11]

Dershowitz, N. and Jouannaud, J.-P.: Rewrite systems, in J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, Elsevier (North-Holland), 1990, Chapt. 6, pp. 244-320.

[12]

Dowek, G.: Lambda-calculus, combinators and the comprehension scheme, in M. Dezan-Ciancaglini and G. Plotkin (eds.), Typed Lambda Calculi and Applications, Lecture Notes in Comput. Sci. 902, 1995, pp. 154-170.

[13]

Dowek, G.: Proof normalization for a first-order formulation of higher-order logic, in E. Gunter and A. Felty (eds.), Theorem Proving in Higher Order Logics, Lecture Notes in Comput. Sci. 1275, 1997, pp. 105-119.

[14]

Dowek, G.: La Part du Calcul, Université de Paris 7, Mémoire d'habilitation, 1999.

[15]

Dowek, G.: Axioms vs. rewrite rules: From completeness to cut elimination, in H. Kirchner and C. Ringeissen (eds.), Frontiers of Combining Systems, Lecture Notes in Artificial Intelligence 1794, Springer-Verlag, 2000, pp. 62-72.

[16]

Dowek, G., Hardin, T. and Kirchner, C.: Theorem proving modulo, Rapport de Recherche 3400, Institut National de Recherche en Informatique et en Automatique, 1998. http://www.inria.fr/rrrt/rr-3400.html.

[17]

Dowek G., Hardin T., and Kirchner C. Higher-order unification via explicit substitutions Inform. and Comput. 2000 157 183-235

[18]

Dowek G., Hardin T., and Kirchner C. HOL-?s, an intentional first-order expression of higher-order logic Math. Structures Comput. Sci. 2001 11 1 21-45

[19]

Dowek, G., Hardin, T. and Kirchner, C.: Theorem proving modulo, revised version, Rapport de Recherche 4861, Institut National de Recherche en Informatique et en Automatique, 2003. http://www.inria.fr/rrrt/rr-4861.html.

[20]

Dowek, G. and Werner, B.: Proof normalization modulo, in Types for Proofs and Programs, Lecture Notes in Comput. Sci. 1657, 1999, pp. 62-77.

[21]

Gallier J. H. Logic for Computer Science: Foundations of Automatic Theorem Proving 1986 New York Harper & Row

[22]

Gallier J., Raatz S., and Snyder W. Aït-Kaci H. and Nivat M. Rigid E-unification and its applications to equational matings Resolution of Equations in Algebraic Structures 1989 New York Academic Press 151-216

[23]

Girard, J.-Y., Lafont, Y. and Taylor, P.: Proofs and Types, Cambridge Tracts Theoret. Comput. Sci. 7, Cambridge University Press, 1989.

[24]

Huet, G.: Constrained resolution: A complete method for type theory, Ph.D. thesis, Case Western Reserve University, 1972.

[25]

Huet, G.: A mechanization of type theory, in Proceeding of the Third International Joint Conference on Artificial Intelligence, 1973, pp. 139-146.

[26]

Huet G. A unification algorithm for typed lambda calculus Theoret. Comput. Sci. 1975 1 1 27-57

[27]

Huet G. Résolution d'equations dans les langages d'ordre 1, 2,...,? 1976 France Université de Paris

[28]

Hullot, J.-M.: Canonical forms and unification, in Proceedings 5th International Conference on Automated Deduction, Les Arcs (France), 1980, pp. 318-334.

[29]

Jaffar, J. and Lassez, J.-L.: Constraint logic programming, in Proceedings of the 14th Annual ACM Symposium on Principles Of Programming Languages, Munich (Germany), 1987, pp. 111-119.

[30]

Jouannaud J.-P. and Kirchner H. Completion of a set of rules modulo a set of equations SIAM J. Comput. 1986 15 4 1155-1194

[31]

Jouannaud J.-P. and Kirchner C. Lassez J.-L. and Plotkin G. Solving equations in abstract algebras: A rule-based survey of unification Computational Logic. Essays in honor of Alan Robinson 1991 Cambridge, MA MIT Press 257-321

[32]

Kirchner, C.: Méthodes et outils de conception systématique d'algorithmes d'unification dans les théories équationnelles, Thèse de Doctorat d'Etat, Université Henri Poincaré - Nancy 1, 1985.

[33]

Kirchner, H.: Orderings in automated theorem proving, in F. Hoffman (ed.), Mathematical Aspects of Artificial Intelligence, Proc. Symposia Appl. Math. 55, Amer. Math. Soc., 1998, pp. 55-95.

[34]

Kirchner C., Kirchner H., and Rusinowitch M. Deduction with symbolic constraints Revue d'Intelligence Artificielle 1990 4 3 9-52 Special issue on Automatic Deduction.

[35]

Kirchner, C. and Ringeissen, C.: Higher-order equational unification via explicit substitutions, in Proceedings 6th International Joint Conference ALP'97-HOA'97, Southampton (UK), Lecture Notes in Comput. Sci. 1298, Springer-Verlag, 1997, pp. 61-75.

[36]

Klop J., van Oostrom V., and van Raamsdonk F. Combinatory reduction systems: Introduction and survey Theoret. Comput. Sci. 1993 121 279-308

[37]

Knuth D. E. and Bendix P. B. Leech J. Simple word problems in universal algebras Computational Problems in Abstract Algebra 1970 Oxford Pergamon Press 263-297

[38]

Kolata, G.: With major math proof, brute computers show flash of reasoning power, New York Times, Tuesday, December 10, 1996.

[39]

Lee S.-J. and Plaisted D. Use of replace rules in theorem proving Methods of Logic in Computer Science 1994 1 2 217-240

[40]

Marché, C.: Normalised rewriting and normalised completion, in S. Abramsky (ed.), Proceedings 9th IEEE Symposium on Logic in Computer Science, Paris, 1994, pp. 394-403.

[41]

McCune W. Solution of the Robbins problem J. Automated Reasoning 1997 19 3 263-276

[42]

Nieuwenhuis, R. and Rubio, A.: AC-superposition with constraints: No AC-unifiers needed, in A. Bundy (ed.), Proceedings 12th International Conference on Automated Deduction, Nancy (France), Lecture Notes in Artificial Intelligence 814, Springer-Verlag, 1994, pp. 545-559.

[43]

Nutt W., Réty P., and Smolka G. Basic narrowing revisited J. Symbolic Comput. 1989 7 3-4 295-318 Special issue on unification. Part one.

[44]

Peterson G. A technique for establishing completeness results in theorem proving with equality SIAM J. Comput. 1983 12 1 82-100

[45]

Peterson G. and Stickel M. E. Complete sets of reductions for some equational theories J. ACM 1981 28 233-264

[46]

Plaisted D. A. and Potter R. C. Term rewriting: Some experimental results J. Symbolic Comput. 1991 11 1-2 149-180

[47]

Plotkin G. Building-in equational theories Machine Intelligence 1972 7 73-90

[48]

Stickel M. Automated deduction by theory resolution J. Automated Reasoning 1985 1 4 285-289

[49]

Stuber, J.: A model-based completeness proof of extended narrowing and resolution, in 1st Int. Joint Conf. on Automated Reasoning (IJCAR-2001), Siena, Italy, Lecture Notes in Comput. Sci. 2083, Springer-Verlag, 2001, pp. 195-210.

[50]

Terese (M. Bezem, J. W. Klop and R. de Vrijer, eds.): Term Rewriting Systems, Cambridge University Press, 2002.

[51]

Vigneron, L.: Positive deduction modulo regular theories, in H. K. Büning (ed.), Annual Conference of the European Association for Computer Science Logic, Lecture Notes in Comput. Sci. 1092, Springer-Verlag, 1995, pp. 468-485. Selected papers.

[52]

Viry P. Equational rules for rewriting logic Theoret. Comput. Sci. 2002 285 2 487-517

Cited By

Cailler JRosain JDelahaye DRobillard SBouziane H(2022)Goéland: A Concurrent Tableau-Based Theorem Prover (System Description)Automated Reasoning10.1007/978-3-031-10769-6_22(359-368)Online publication date: 8-Aug-2022
https://dl.acm.org/doi/10.1007/978-3-031-10769-6_22
Dowek G(2022)From the Universality of Mathematical Truth to the Interoperability of Proof SystemsAutomated Reasoning10.1007/978-3-031-10769-6_2(8-11)Online publication date: 8-Aug-2022
https://dl.acm.org/doi/10.1007/978-3-031-10769-6_2
Kim DLynch C(2021)Equational Theorem Proving ModuloAutomated Deduction – CADE 2810.1007/978-3-030-79876-5_10(166-182)Online publication date: 12-Jul-2021
https://dl.acm.org/doi/10.1007/978-3-030-79876-5_10
Show More Cited By

Index Terms

Theorem Proving Modulo

Index terms have been assigned to the content through auto-classification.

Recommendations

Resolution is Cut-Free

In this article, we show that the extension of the resolution proof system to deduction modulo is equivalent to the cut-free fragment of the sequent calculus modulo. The result is obtained through a syntactic translation, without using any cut-...
Extensional Higher-Order Paramodulation in Leo-III
Abstract
Leo-III is an automated theorem prover for extensional type theory with Henkin semantics and choice. Reasoning with primitive equality is enabled by adapting paramodulation-based proof search to higher-order logic. The prover may cooperate with ...
Cut Elimination in Deduction Modulo by Abstract Completion
LFCS '07: Proceedings of the international symposium on Logical Foundations of Computer Science

Deduction Modulo implements Poincarés principle by identifying deduction and computation as different paradigms and making their interaction possible. This leads to logical systems like the sequent calculus or natural deduction modulo. Even if deduction ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of Automated Reasoning

Journal of Automated Reasoning Volume 31, Issue 1

Sep 2003

101 pages

ISSN:0168-7433

Issue’s Table of Contents

© Kluwer Academic Publishers 2003.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 September 2003

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

63
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Cailler JRosain JDelahaye DRobillard SBouziane H(2022)Goéland: A Concurrent Tableau-Based Theorem Prover (System Description)Automated Reasoning10.1007/978-3-031-10769-6_22(359-368)Online publication date: 8-Aug-2022
https://dl.acm.org/doi/10.1007/978-3-031-10769-6_22
Dowek G(2022)From the Universality of Mathematical Truth to the Interoperability of Proof SystemsAutomated Reasoning10.1007/978-3-031-10769-6_2(8-11)Online publication date: 8-Aug-2022
https://dl.acm.org/doi/10.1007/978-3-031-10769-6_2
Kim DLynch C(2021)Equational Theorem Proving ModuloAutomated Deduction – CADE 2810.1007/978-3-030-79876-5_10(166-182)Online publication date: 12-Jul-2021
https://dl.acm.org/doi/10.1007/978-3-030-79876-5_10
Sottile CDíaz-Caro AMartínez López P(2020)Polymorphic System IProceedings of the 32nd Symposium on Implementation and Application of Functional Languages10.1145/3462172.3462198(127-137)Online publication date: 2-Sep-2020
https://dl.acm.org/doi/10.1145/3462172.3462198
Burel G(2020)Linking Focusing and Resolution with SelectionACM Transactions on Computational Logic10.1145/337327621:3(1-30)Online publication date: 20-Feb-2020
https://dl.acm.org/doi/10.1145/3373276
Burel GBury GCauderlier RDelahaye DHalmagrand PHermant O(2020)First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets PracticeJournal of Automated Reasoning10.1007/s10817-019-09533-z64:6(1001-1050)Online publication date: 1-Aug-2020
https://dl.acm.org/doi/10.1007/s10817-019-09533-z
Bhayat AReger G(2019)Restricted Combinatory UnificationAutomated Deduction – CADE 2710.1007/978-3-030-29436-6_5(74-93)Online publication date: 27-Aug-2019
https://dl.acm.org/doi/10.1007/978-3-030-29436-6_5
Sutcliffe G(2017)The CADE-26 automated theorem proving system competition – CASC-26AI Communications10.3233/AIC-17074430:6(419-432)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.3233/AIC-170744
Platzer A(2017)A Complete Uniform Substitution Calculus for Differential Dynamic LogicJournal of Automated Reasoning10.1007/s10817-016-9385-159:2(219-265)Online publication date: 1-Aug-2017
https://dl.acm.org/doi/10.1007/s10817-016-9385-1
Chihani ZMiller DRenaud F(2017)A Semantic Framework for Proof EvidenceJournal of Automated Reasoning10.1007/s10817-016-9380-659:3(287-330)Online publication date: 1-Oct-2017
https://dl.acm.org/doi/10.1007/s10817-016-9380-6
Show More Cited By

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents