Elamur Research⌕
☰
home / papers / 1990 / Isabelle: The Next 700 Theorem Provers

Isabelle: The Next 700 Theorem Provers

Paper · 1990 · Lawrence C. Paulson

Summary

The paper surveys Isabelle, a generic interactive theorem prover. Rather than building a separate LCF-style system for each new logic, Isabelle tackles problems common to all logics once, so that each logic only needs its own specific parts. Paulson tells the system's history, starting from Milner's Edinburgh LCF with its tactics and tacticals, and frankly records the mistakes made along the way.

The central design choice is to write inference rules literally, as premises plus a conclusion. Proofs are then built by joining rules through Huet's higher-order unification. The early system, Isabelle-86, was later replaced by a meta-logic with implication, a universal quantifier and equality. This meta-logic handles assumption discharge, eigenvariables, natural deduction and derived rules cleanly. A comparison is drawn between this method and the Logical Framework developed at Edinburgh.

Several object-logics are presented, including Constructive Type Theory, first-order logics and Zermelo-Fraenkel set theory. The paper matters because it shows one small, generic kernel can support many formal theories with reasonable automation. It also argues that powerful tools remain more important than a friendly interface.

Key points

  • Isabelle is written entirely in Standard ML. Its core technique is higher-order unification (Huet, 1975), which is undecidable in theory but proved reliable in practice.
  • In Isabelle-86, repeated rule application in the sequent calculus automatically solved roughly 35 of Pelletier's (1986) problems. Sequence variables were obtained by encoding lists so that unification behaves associatively.
  • Early versions were very slow. Removing Skolem terms and replacing structure sharing with copying made the system both simpler and faster.
  • The newer meta-logic is a fragment of higher-order logic built from implication (⟹), universal quantification (⋀) and equality (≡).
  • The Zermelo-Fraenkel set theory development includes about 60 examples, such as the justification of the pairing definition ⟨a,b⟩ = {{a},{a,b}}. Users extended the system further: Noël developed fixedpoint theory, and Nipkow (1989) built rewriting tactics.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓École Polytechnique Fédérale de LausanneLausanne · Switzerland56 works · 8,189 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Lawrence C. Paulson. 1990. Isabelle: The Next 700 Theorem Provers. arXiv:cs/9301106 (published in P. Odifreddi (editor), Logic and Computer Science (Academic Press, 1990), 361-386).

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.cs/9301106 · arXiv cs/9301106

@misc{paulson1990isabelle,
  title = {{Isabelle: The Next 700 Theorem Provers}},
  author = {Lawrence C. Paulson},
  year = {1990},
  doi = {10.48550/arxiv.cs/9301106},
  eprint = {cs/9301106},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.cs/9301106}
}

References

25 references, 0 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Peter B. Andrews, Dale A. Miller, Eve L. Cohen, and Frank Pfenning (1984). Automating higher-order logic. In W. W. Bledsoe and D. W. Loveland, editors, Automated Theorem Proving: After 25 Years, pages 169–192, American Mathematical Society. find
  2. Peter B. Andrews (1986). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press. find
  3. A. Avron, F. A. Honsell, and I. A. Mason (1987). Using typed lambda calculus to implement formal systems on a machine. Report ecs-lfcs-87-31. Computer Science Department, University of Edinburgh. find
  4. Graham Birtwistle and P. A. Subrahmanyam (1988), editors. VLSI Specification, Verification and Synthesis. Kluwer Academic Publishers. find
  5. Alonzo Church (1940). A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68. find
  6. R. L. Constable et al. (1986). Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall International. find
  7. N. G. de Bruijn (1972). Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem. Indagationes Mathematicae, 34:381–392. find
  8. Amy Felty and Dale Miller (1988). Specifying theorem provers in a higher-order logic programming language. In E. Lusk and R. Overbeek, editors, 9th International Conference on Automated Deduction, pages 61–80, Springer-Verlag. LNCS 310. find
  9. Michael J. C. Gordon (1988). HOL: a proof generating system for higher-order logic. In Birtwistle and Subrahmanyam (1988), pages 73–128. find
  10. R. Harper, F. Honsell and G. Plotkin (1987). A Framework for Defining Logics. Symposium on Logic in Computer Science. ieee Computer Society Press, 194–204. find
  11. G. P. Huet (1975). A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57. find
  12. G. P. Huet and B. Lang (1978). Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11:31–55. find
  13. Per Martin-Löf (1984). Intuitionistic type theory. Bibliopolis. find
  14. Tobias Nipkow (1989). Equational reasoning in Isabelle. Science of Computer Programming, 12:123–149. find
  15. B. Nordström and J. M. Smith (1984). Propositions and specifications of programs in Martin-Löf’s type theory. BIT, 24:288–301. find
  16. L. C. Paulson (1986). Natural deduction as higher-order resolution. Journal of Logic Programming, 3:237–258. find
  17. L. C. Paulson (1987). Logic and Computation: Interactive proof with Cambridge LCF. Cambridge University Press. find
  18. L. C. Paulson (1988). A preliminary user’s manual for Isabelle. Technical Report 133, University of Cambridge Computer Laboratory. find
  19. L. C. Paulson (1989). The foundation of a generic theorem prover. Journal of Automated Reasoning, 5:363–397. find
  20. F. J. Pelletier (1986). Seventy-five problems for testing automatic theorem provers. Journal of Automated Reasoning, 2:191–216. Errata, JAR 4 (1988), 236–236. find
  21. D. Prawitz (1965). Natural Deduction: A Proof-theoretical Study. Almquist and Wiksell. find
  22. P. Schroeder-Heister (1984). Generalized rules for quantifiers and the completeness of the intuitionistic operators &, ∨, ⊃, ⊥, ∀, ∃. In Computation and Proof Theory: Logic Colloquium ’83, pages 399–426, Springer-Verlag. Lecture Notes in Mathematics 1104. find
  23. Stefan SokoÃlowski (1987). Soundness of Hoare’s logic: an automatic proof using LCF. ACM Transactions on Programming Languages and Systems, 9:100–120. find
  24. G. Takeuti (1987). Proof Theory, 2nd edition. North Holland. find
  25. Å. Wikström (1987). Functional Programming using ML. Prentice-Hall International. find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/paulson-2000-isabelle-next-700-theorem-provers/