Skip to main content
Log in

Comparing Approaches To Resolution Based Higher-Order Theorem Proving

  • Published:
Synthese Aims and scope Submit manuscript

Abstract

We investigate several approaches to resolution based automated theoremproving in classical higher-order logic (based on Church's simply typedλ-calculus) and discuss their requirements with respect to Henkincompleteness and full extensionality. In particular we focus on Andrews' higher-order resolution (Andrews 1971), Huet's constrained resolution (Huet1972), higher-order E-resolution, and extensional higher-order resolution(Benzmüller and Kohlhase 1997). With the help of examples we illustratethe parallels and differences of the extensionality treatment of these approachesand demonstrate that extensional higher-order resolution is the sole approach thatcan completely avoid additional extensionality axioms.

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

Access this article

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

REFERENCES

  • Andrews, P, B.: 1971, ‘Resolution in Type Theory’, Journal of Symbolic Logic 36, 414–432.

    Google Scholar 

  • Andrews, P. B.: 1972, ‘General Models and Extensionality’, Journal of Symbolic Logic 37, 395–397.

    Google Scholar 

  • Andrews, P. B.: 1973, Letter to Roger Hindley dated January 22.

  • Andrews, P. B.: ‘Refutations by Matings’, IEEE Transactions on Computers C-25, 801–807.

  • Andrews, P. B.: 1989, ‘On Connections and Higher Order Logic’, Journal of Automated Reasoning 5, 257–291.

    Google Scholar 

  • Andrews, P. B., Bishop, M., Issar, S., Nesmith, D., Pfenning, F., and Xi, H.: 1996, ‘TPS: A Theorem Proving System for Classical Type Theory’, Journal of Automated Reasoning 16, 321–353.

    Google Scholar 

  • Barendregt, H. P.: 1984, The Lambda Calculus — Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics 103, Amsterdam.

  • Benzmüller, C.: 1997, A calculus and a System Architecture for Extensional Higher-order Resolution, Research Report 97-198, Department of Mathematical Sciences, Carnegie Mellon University.

  • Benzmüller, C.: 1999a, Equality and Extensionality in Automated Higher-Order Theorem Proving, Ph.D. thesis, Technische Fakultät, Universität des Saarlandes.

  • Benzmüller, C.: 1999b, in H. Ganzinger (ed.), Proceedings of the 16th Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 1632, pp. 399–413, Springer.

  • Benzmüller, C. and Kohlhase, M.: 1997, ‘Model Existence for Higher-Order Logic’, SEKI-Report SR-97-09, Fachbereich Informatik, Universität des Saarlandes.

  • Benzmüller, C. and Kohlhase, M.: 1998a, ‘Extensional Higher-order Resolution’, in Kirchner and Kirchner (eds.), Proceedings of the 15th Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 1421, pp.56–72, Springer.

  • Benzmüller, C. and Kohlhase, M. 1998b, ‘LEO — A Higher-order Theorem Prover, in Kirchner and Kirchner (eds.), Proceedings of the 15th Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 1421, pp. 139–144, Springer.

  • Baader, F. and Siekmann, J.: 1994, ‘Unification Theory’, in D. M. Gabbay, C. J. Hogger, J. A. Robinson (eds.), Handbook of Logic in Artificial Intelligence and Logic Programming, Volume 2: Deduction Methodologies, Oxford, Chapter 2.2

  • Church, A.: 1940, ‘A formulation of the Simple Theory of Types’, Journal of Symbolic Logic 5, 56–68.

    Google Scholar 

  • Dowek, G., Hardin, T., and Kirchner, C.: 1998, Theorem Proving Modulo, Rapport de Recherche 3400, Institut National de Recherche en Informatique et en Automatique.

  • Dougherty, D. and Johann, P.: 1992, ‘A Combinatory Logic Approach to Higher-order E-unification’, in D. Kapur (ed.), Proceedings of the 11th Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 607, pp. 79–93, Springer.

  • Goldfarb, W. D. 1981, ‘The Undecidability of the Second-order Unification Problem’, Theoretical Computer Science 13, 225–230.

    Google Scholar 

  • Henkin, L.: 1950, ‘Completeness in the Theory of Types’, Journal of Symbolic Logic 15, 81–91.

    Google Scholar 

  • Huet, G. P.: 1972, Constrained Resolution: A Complete Method for Higher Order Logic, Ph.D. thesis, Case Western Reserve University.

  • Huet, G. P.: 1973, ‘A Mechanization of Type Theory’, in D. E. Walker and L. Norton (eds.), Proceedings of the 3rd International Joint Conference on Artificial Intelligence, pp. 139–146.

  • Huet, G. P.: 1973, ‘The Undecidability of Unification in Third Order Logic’, Information and Control 22, 257–267.

    Google Scholar 

  • Huet, G. P.: 1975, ‘A Unification Algorithm for Typed λ-calculus’, Theoretical Computer Science 1, 27–57.

    Google Scholar 

  • Jensen, D. C. and Pietrzykowski, T.: 1972, ‘A Complete Mechanization of ω-order Type Theory’, in Proceedings of the ACM annual Conference, volume 1, 89–92.

    Google Scholar 

  • Jensen, D. C. and Pietrzykowski, T.: 1976, ‘Mechanizing ω-order Type Theory through Unification’, Theoretical Computer Science 3, 123–171.

    Google Scholar 

  • Kohlhase, M.: 1994, A Mechanization of Sorted Higher-Order Logic Based on the Resolution Principle, Ph.D. thesis, Fachbereich Informatik, Universität des Saarlandes.

  • Kohlhase, M.: 1995, ‘Higher-Order Tableaux’, in P. Baumgartner, R. Hähnle, and J. Posegga (eds.), Theorem Proving with Analytic Tableaux and Related Methods, Lecture Notes in Artificial Intelligence 918, pp. 294–309, Springer.

  • Lucchesi, C. L.: 1972, The Undecidability of the Unification Problem for Third Order Languages, Report CSRR 2059, University of Waterloo, Waterloo, Canada.

    Google Scholar 

  • Miller, D.: 1983, Proofs in Higher-Order Logic, Ph.D. thesis, Carnegie Mellon University.

  • Nipkow, T.: 1995, ‘Higher-order Rewrite Systems’, in J. Hsiang (ed.), Rewriting Techniques and Applications, 6th International Conference, Lecture Notes in Computer Science 914, Springer.

  • Nipkow, T. and Prehofer, C.: 1998, ‘Higher-order Rewriting and Equational Reasoning’, in W. Bibel and P. Schmitt (eds.), Automated Deduction — A Basis for Applications, Dordrecht, Applied Logic Series, pp. 399–430.

  • Nipkow, T. and Qian, Z,: 1991, ‘Modular Higher-order E-unification’, in R. V. Book (ed.), Proceedings of the 4th International Conference on Rewriting Techniques and Applications, Lecture Notes in Artificial Intelligence 488, pp. 200–214, Springer.

  • Prehofer, C.: 1998, Solving Higher-Order Equations: From Logic to Programming, Progress in theoretical computer science, Birkhäuser.

  • Qian, Z. and Wang K.: 1996, ‘Modular Higher-order Equational Preunification’, Journal of Symbolic Computation 22, 401–424.

    Google Scholar 

  • Robinson, J. A.: 1965, ‘A Machine-oriented Logic Based on the Resolution Principle’, Journal of the Association for Computing Machinery 12, 23–41.

    Google Scholar 

  • Siekmann, J. H.: 1989, ‘Unification Theory’, Journal of Symbolic Computation 7, 207–274.

    Google Scholar 

  • Smullyan, R. M. 1963, ‘A Unifying Principle for Quantification Theory’, Proceedings of the National Acadamy of Sciences, USA 49, pp. 828–832.

    Google Scholar 

  • Snyder, W.: 1990, ‘Higher Order E-unification’, in M. Stickel (ed.), Proceedings of the 10th Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 449, pp. 573–578, Springer.

  • Snyder, W. and Gallier, J.: 1989, ‘Higher-order Unification Revisited: Complete Sets of Transformations’, Journal of Symbolic Computation 8, 101–140.

    Google Scholar 

  • Snyder, W. and Lynch, C.: 1991, ‘Goal-directed Strategies for Paramodulation’, in R. V. Book (ed.), Proceedings of the 4th International Conference on Rewriting Techniques and Applications, Lecture Notes in Artificial Intelligence 488, pp. 200–214, Springer.

  • Wolfram, D. A.: 1993, The Clausal Theory of Types, Cambridge, Cambridge Tracts in Theoretical Computer Science 21.

Download references

Author information

Authors and Affiliations

Authors

Rights and permissions

Reprints and permissions

About this article

Cite this article

Benzmüller, C. Comparing Approaches To Resolution Based Higher-Order Theorem Proving. Synthese 133, 203–335 (2002). https://doi.org/10.1023/A:1020840027781

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1023/A:1020840027781

Keywords

Navigation