Primary evidence
- HOL: A Proof Generating System for Higher-Order LogicS1 · Primary research · Paper · 1988-01-01
- HOL: A proof generating system for higher-order logic — Technical Report 103S1 · Primary research · Paper
HOL consolidates LCF-style mechanized proof for higher-order logic
HOL combined a small trusted logical basis, ML programming and tactics/tacticals for goal-directed interactive proof in higher-order logic.
What happened?
Mike Gordon's public system descriptions documented HOL as an LCF-derived proof-generating system for higher-order logic; the 1988 archival chapter provides a precise publication anchor after the January 1987 Cambridge technical report.
Why it matters
HOL and its descendants supplied formal corpora and interactive environments later used by systems such as TacticToe, HOL(y)Hammer and learning-based theorem provers.
Significance rationale: HOL adapted the LCF architecture to classical higher-order logic and became a major proof-assistant family supporting mechanized mathematics, hardware verification and later AI theorem-proving research.
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
- Humans directed proofs through tactics while the system mechanically executed inference and checked resulting derivations.
- Human contribution
- Mike Gordon and the HOL/LCF community designed the logic, trusted implementation and tactic-based interaction model.
- Verification
- Paper released · E2 · Research record · No formal assurance
- Last reviewed
- 2026-09-15
Technical details
- Systems
- hol, lcf
- Organizations
- university-of-cambridge
- Problems
- higher-order-logic-theorem-proving
- Methods
- interactive-theorem-proving, tactics, trusted-kernel
Sources & artifacts
- HOL: A Proof Generating System for Higher-Order LogicS1 · Primary research · Paper · accessed 2026-09-15
- HOL: A proof generating system for higher-order logic — Technical Report 103S1 · Primary research · Paper · accessed 2026-09-15
Verification history
- 1988-01-01 · Paper released · E2 · Research record
The archival HOL chapter and Cambridge technical-report record establish the system architecture and higher-order logic implementation.
Corrections
No corrections recorded.