Primary evidence
- The PLTP ArchiveS1 · Primary research · Repository
The Edinburgh Pure Lisp Theorem Prover brings automated induction to program reasoning
PLTP targeted properties of recursively defined programs that resolution-based first-order provers handled poorly, using domain-specific proof procedures centered on simplification and induction.
What happened?
Boyer and Moore presented “Proving Theorems about LISP Functions” at IJCAI-73, documenting the Edinburgh Pure Lisp Theorem Prover developed in 1972–1973 and its automated use of induction, rewriting and symbolic evaluation.
Why it matters
It established a long-running architecture for automated inductive theorem proving and program verification that evolved into influential later systems.
Significance rationale: Boyer and Moore's PLTP established a durable automated-induction lineage for reasoning about recursive Lisp functions, preceding the later Boyer–Moore prover, NQTHM and ACL2.
Historical context
Earlier developments
—
Later developments
—
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E3 · Inspectable artifact
- AI role
- Autonomous primary role
- Formal assurance
- Artifact available
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Formal, Symbolic
- AI contribution
- The prover automatically simplified formulas, selected induction schemes and searched for proofs of recursive-function properties.
- Human contribution
- Robert Boyer and J Strother Moore designed and implemented the logic, heuristics and proof procedures.
- Verification
- Paper released · E3 · Inspectable artifact · Artifact available
- Last reviewed
- 2026-09-15
Technical details
- Systems
- pltp
- Organizations
- university-of-edinburgh
- Problems
- inductive-theorem-proving, program-verification
- Methods
- mathematical-induction, rewriting, symbolic-evaluation
Sources & artifacts
- The PLTP ArchiveS1 · Primary research · Repository · accessed 2026-09-15
- PLTP 1973 source listings and reconstructionsArtifact · Code
Verification history
- 1973-08-20 · Paper released · E2 · Research record
The IJCAI-73 paper documents PLTP and its theorem-proving methods.
- 2026-09-15 · Paper released · E3 · Inspectable artifact
The UT Austin PLTP archive preserves original 1973 source listings and modern transcriptions/reconstructions.
Corrections
No corrections recorded.