Primary evidence
- Isabelle — The Next Seven Hundred Theorem ProversS1 · Primary research · Paper · 1988-05-23
Isabelle develops a generic theorem-proving framework across object logics
Isabelle used higher-order unification and a generic meta-level architecture to encode and reason within several object logics, with tactics and tacticals providing automation.
What happened?
Isabelle was first made publicly available in 1986; Paulson's CADE-9 system abstract on 23 May 1988 provides the precise public research anchor used for this canonical Event date.
Why it matters
Isabelle later supported major formal verification projects and created the environment in which Sledgehammer and other ATP/ML integrations matured.
Significance rationale: Isabelle generalized the LCF tradition into a theorem-proving framework supporting multiple object logics and substantial tactic automation, later becoming a major platform for formal mathematics and AI-assisted proving.
Historical context
Earlier developments
Later developments
—
Related milestones
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E2 · Research record
- AI role
- Human–AI collaboration
- Formal assurance
- No formal assurance
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Formal, Symbolic
- AI contribution
- Users supplied formal goals and guidance while the system executed logical inference, unification and tactic automation.
- Human contribution
- Lawrence Paulson and collaborators designed the generic architecture, object-logic encodings and automation mechanisms.
- Verification
- Paper released · E2 · Research record · No formal assurance
- Last reviewed
- 2026-09-15
Technical details
- Systems
- isabelle
- Organizations
- university-of-cambridge
- Problems
- generic-theorem-proving
- Methods
- higher-order-unification, tactics, interactive-theorem-proving
Sources & artifacts
- Isabelle — The Next Seven Hundred Theorem ProversS1 · Primary research · Paper · accessed 2026-09-15
- Older Isabelle ReleasesS2 · Official institutional · Official announcement · accessed 2026-09-15
Verification history
- 1988-05-23 · Paper released · E2 · Research record
The CADE-9 proceedings establish the public system description; official Isabelle archives corroborate an earlier Isabelle86 release.
Corrections
No corrections recorded.