A mechanization of sorted higher-order logic based on the resolution principle

Abstract

The usage of sorts in first-order automated deduction has brought greater conciseness of representation and a considerable gain in efficiency by reducing the search spaces involved. This suggests that sort information can be employed in higher-order theorem proving with similar results.

Categories

Keywords

Reprint years

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 101,072

External links

  • This entry has no external links. Add one.
Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

  • Only published works are available at libraries.

My notes

Similar books and articles

Comparing Approaches To Resolution Based Higher-Order Theorem Proving.Christoph Benzmüller - 2002 - Synthese 133 (1-2):203-335.
Higher-order automated theorem proving.Michael Kohlhase - unknown
Automated Deduction - CADE-15: 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings.Claude Kirchner & Helene Kirchner - 1998 - Springer Verlag.
The Clausal Theory of Types.D. A. Wolfram - 1993 - Cambridge University Press.
Effective Higher-Order Automated Theorem Proving with integrated Descente Infinie and Presburger Arithmetic LEO-III.Benzmüller Christoph & Wirth Claus-Peter - 2009
Equality and Extensionality in Higher-Order Theorem Proving.Benzmüller Christoph - 1999 - Dissertation, Naturwissenschaftlich-Technische Fakultät I, Saarland University, Saarbrücken, Germany
Automated Deduction, Cade-12.: 12th International Conference on Automated Deduction, Nancy, France, June 26 - July 1, 1994. Proceedings.Alan Bundy - 1994 - Springer Verlag.
System description: { A higher-order theorem prover?Michael Kohlhase - manuscript
Automated Deduction in Classical and Non-Classical Logics: Selected Papers.Ricardo Caferra & Gernot Salzer - 2000 - Springer Verlag.
Higher Order Logic Theorem Proving and Its Applications: 8th International Workshop, Aspen Grove, UT, USA, September 11 - 14, 1995. Proceedings.E. Thomas Schubert, Phillip J. Windley, James Alves-Foss & International Workshop on Higher Order Logic Theorum Proving and its Applications - 1995 - Springer Verlag.

Analytics

Added to PP
2010-02-07

Downloads
441 (#65,148)

6 months
441 (#3,570)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Cut-Elimination for Quantified Conditional Logic.Christoph Benzmüller - 2017 - Journal of Philosophical Logic 46 (3):333-353.
Higher-Order Multi-Valued Resolution.Michael Kohlhase - 1999 - Journal of Applied Non-Classical Logics 9 (4):455-477.

View all 7 citations / Add more citations

References found in this work

No references found.

Add more references