Abstract
We provide techniques to integrate resolution logic with equality in type theory. The results may be rendered as follows.
-
A clausification procedure in type theory, equipped with a correctness proof, all encoded using higher-order primitive recursion.
-
A novel representation of clauses in minimal logic such that the λ-representation of resolution proofs is linear in the size of the premisses.
-
A translation of resolution proofs into lambda terms, yielding a verification procedure for those proofs.
-
The power of resolution theorem provers becomes available in interactive proof construction systems based on type theory.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Bliksem is available at http://www.mpi-sb.mpg.de/~bliksem
de Bruijn, N.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation. Indagationes Mathematicae 34, 381–392 (1972)
Barras, B., Boutin, S., Cornes, C., Courant, J., Filliâtre, J.-C., Giménez, E., Herbelin, H., Huet, G., Muñez, C., Murthy, C., Parent, C., Paulin-Mohring, C., Saïbi, A., Werner, B.: The Coq Proof Assistant Reference Manual, version 6.2.4. INRIA (1998), Available at: ftp.inria.fr/INRIA/coq/V6.2.4/doc/Reference-Manual.ps
Hendriks, D.: Clausification of First-Order Formulae, Representation & Correctness in Type Theory. Master’s Thesis. Utrecht University (1998), http://www.phil.uu.nl/~hendriks/thesis.ps.gz
Huang, X.: Translating machine-generated resolution proofs into ND-proofs at the assertion level. In: Foo, N.Y., Göbel, R. (eds.) PRICAI 1996. LNCS, vol. 1114, pp. 399–410. Springer, Heidelberg (1996)
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)
McCune,W., Shumsky,O.: IVY: A preprocessor and proof checker for firstorder logic.(Preprint ANL/MCS-P775-0899) Argonne National Laboratory, Argonne IL (1999)
Nadathur, G., Miller, D.: Higher-order logic programming. In: Gabbay, D. (ed.) Handbook of logic in artificial intelligence, vol. 5, pp. 499–590. Clarendon Press, Oxford (1998)
Omega can be found on, http://www.ags.uni-sb.de/~omega/
Pfenning, F.: Analytic and non-analytic proofs. In: Shostak, R.E. (ed.) CADE 1984. LNCS, vol. 170, pp. 394–413. Springer, Heidelberg (1984)
Smith, J., Tammet, T.: Optimized encodings of fragments of type theory in first-order logic. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol. 1158, pp. 265–287. Springer, Heidelberg (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bezem, M., Hendriks, D., de Nivelle, H. (2000). Automated Proof Construction in Type Theory Using Resolution. In: McAllester, D. (eds) Automated Deduction - CADE-17. CADE 2000. Lecture Notes in Computer Science(), vol 1831. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10721959_10
Download citation
DOI: https://doi.org/10.1007/10721959_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67664-5
Online ISBN: 978-3-540-45101-3
eBook Packages: Springer Book Archive