×
Paulson, Lawrence C.

The foundation of a generic theorem prover. (English) Zbl 0679.68173

J. Autom. Reasoning 5, No. 3, 363-397 (1989).
The logical framework of the interactive theorem prover ISABELLE is laid down. ISABELLE is constructed to support a variety of logics: Martin- Löf’s type theory, Zermelo-Fraenkel set theory, intuitionistic and classical sequent calculi. It is implemented in Standard ML.
To meet the needs of a generic theorem prover like ISABELLE a higher- order logic or meta-logic is established to build proofs in those various object-logics. On the meta-level ISABELLE incorporates intuitionistic higher-order logic to ease proofs by deductions, i.e. rules are represented as propositions and combined to yield proofs.
Natural deduction, object-level backwards proofs with examples from propositional and first order logic both of them in classical as well as intuitionistic form are highlighted as practical applications of ISABELLE. Theoretical issues like sound- and completeness are shown to remain valid. Advantages over LCF, AUTOMATH and an earlier version of ISABELLE - ISABELLE-86 - are considered with respect to computational complexity of proof constructions.
Reviewer: R.Horsch

Cited in 50 Documents

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Keywords:

meta reasoning; higher-order unification; natural deduction; logical framework; ISABELLE; Standard ML; higher-order logic; LCF

Software:

Cambridge LCF; Nuprl; HOL; Automath; ETPS
PDF BibTeX XML Cite
\textit{L. C. Paulson}, J. Autom. Reasoning 5, No. 3, 363--397 (1989; Zbl 0679.68173)
Full Text: DOI
  • logo of hbz
  • logo of WorldCat

References:

[1] Andrews, P. B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Academic Press (1986). · Zbl 0617.03001
[2] Andrews, P. B., Miller, D. A., Cohen, E. L., and Pfenning, F.: ?Automating higher-order logic?, in: Bledsoe, W. W. and Loveland, D. W. (eds.) Automated Theorem Proving: After 25 Years, American Mathematical Society (1984) pp. 169-192. · Zbl 0551.68075
[3] Avron, A., Honsell, F. A., and Mason, I. A.: ?Using typed lambda calculus to implement formal systems on a machine.? Report ECS-LFCS-87-31, Computer Science Department, University of Edinburgh (1987). · Zbl 0784.68072
[4] Barwise, J. (ed.): Handbook of Mathematical Logic, North-Holland (1977).
[5] Barwise, J.: ?An introduction to first-order logic?, in: Barwise [4], pp. 5-46.
[6] Birtwistle, G. and Subrahmanyam, P. A. (eds.): VLSI Specification, Verification and Synthesis, Kluwer Academic Publishers (1988). · Zbl 0705.68006
[7] de Bruijn, N. G.: ?A survey of the project AUTOMATH?, in: Seldin and Hindley [35], pp. 579-606.
[8] Constable, R. L., et al.: Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall (1986).
[9] Coquand, Th. and Huet, G.: ?The calculus of constructions?, Information and Computation 76, 95-120 (1988). · Zbl 0654.03045
[10] Coquand, Th. and Huet, G., ?Constructions: a higher order proof system for mechanizing mathematics?, in: Buchberger, B., editor, EUROCAL ’85: European Conference on Computer Algebra, Volume 1: Invited lectures, Springer (1985), 151-184. · Zbl 0581.03007
[11] Dummett, M.: Elements of Intuitionism, Oxford University Press (1977). · Zbl 0358.02032
[12] Felty, A. and Miller, D.: ?Specifying theorem provers in a higher-order logic programming language?, in Ninth Conference on Automated Deduction, Lusk, E. and Overbeek, R. (eds.), Springer (1988), pp. 61-80. · Zbl 0645.68097
[13] Gordon, M. J. C., ?HOL: A proof generating system for higher-order logic?, in: Birtwistle and Subrahmanyam [6], pp. 79-128.
[14] de Groote, Ph., ?How I spent my time in Cambridge with Isabelle?, Report RR 87-1, Unité d’informatique, Université Catholique de Louvain, Belgium (1987).
[15] Harper, R., Honsell, F., and Plotkin, G.: ?A Framework for Defining Logics?, Proceedings of a symposium on Logic in Computer Science (IEEE, 1987), pp. 194-204. · Zbl 0778.03004
[16] Hindley, J. R. and Seldin, J. P.: Introduction to Combinators and ?-calculus, Cambridge University Press (1986). · Zbl 0614.03014
[17] Hoare, C. A. R. and Shepherdson, J. C. (eds.); Mathematical Logic and Programming Languages, Prentice-Hall (1985). · Zbl 0626.68003
[18] Howard, W. A.: ?The formulae-as-types notion of construction?, in: Seldin and Hindley [35], pp. 479-490.
[19] Huet, G. P.: ?A unification algorithm for typed ?-calculus?, Theoretical Computer Science 1, 27-57 (1975). · Zbl 0337.68027
[20] Huet, G. P. and Lang, B.: ?Proving and applying program transformations expressed with second-order patterns?, Acta Informatica 11 (1978) 31-55. · Zbl 0389.68008
[21] Jutting, L. S.: Checking Landau’s ?Grundlagen? in the AUTOMATH system, Ph.D. Thesis, Technische Hogeschool, Eindhoven (1977). · Zbl 0352.68105
[22] Lambek, J. and Scott, P. J.: Introduction to Higher Order Categorical Logic, Cambridge University Press (1986). · Zbl 0596.03002
[23] Martin-Löf, P.: ?Constructive mathematics and computer programming?, in: Hoare and Shepherdson [17], pp. 167-184. · Zbl 0443.68039
[24] Martin-Löf, P.: ?On the meanings of the logical constants and the justifications of the logical laws,? Report, Department of Mathematics, University of Stockholm (1986). · Zbl 0593.03005
[25] Martin-Löf, P.: ?Amendment to intuitionistic type theory?, Lecture notes obtained from P. Dybjer, Computer Science Department, Chalmers University, Gothenburg (1986).
[26] Milner, R.: ?The use of machines to assist in rigorous proof?, in: Hoare and Shepherdson [17], pp. 77-88. · Zbl 0572.68078
[27] Nordström, B. and Smith, J. M.: ?Propositions and specifications of programs in Martin-Löf’s type theory?, BIT 24 (1984) 288-301. · Zbl 0551.68027
[28] Paulson, L. C.: ?Natural deduction as higher-order resolution?, Journal of Logic Programming 3 (1986) 237-258. · Zbl 0613.68035
[29] Paulson, L. C.: Logic and Computation: Interactive Proof with Cambridge LCF, Cambridge University Press (1987). · Zbl 0645.68041
[30] Paulson, L. C.: ?A preliminary user’s manual for Isabelle?, Report 133, Computer Laboratory, University of Cambridge (1988).
[31] Prawitz, D.: Natural Deduction: A Proof-theoretical Study, Almquist and Wiksell (1965). · Zbl 0173.00205
[32] Prawitz, D.: ?Ideas and results in proof theory?, in: Fenstad, J. E. (ed.): Proceedings of the Second Scandinavian Logic Symposium, North-Holland (1971), pp. 235-308. · Zbl 0226.02031
[33] Schroeder-Heister, P.: ?A natural extension of natural deduction?, Journal of Symbolic Logic 49 (1984) 1284-1300. · Zbl 0574.03045
[34] Schroeder-Heister, P.: ?Generalized rules for quantifiers and the completeness of the intuitionistic operators &, ?, ?, ?, ?, ??, in: M. M. Richter et al. (eds.): Logic Colloquium ’83, Springer Lecture Notes in Mathematics 1104 (1984). · Zbl 0562.03028
[35] Seldin, J. P. and Hindley, J. R.: To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press (1980). · Zbl 0469.03006
[36] Takeuti, G.: Proof Theory (2nd edition), North Holland (1987). · Zbl 0609.03019
[37] Whitehead, A. N. and Russell, B.: Principia Mathematica, Paperback edition to ?56, Cambridge University Press (1962). · Zbl 0101.24902
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.