Milestones from the Pure Lisp Theorem Prover to ACL2
From MaRDI portal
Publication:2280212
DOI10.1007/s00165-019-00490-3zbMath1427.68348OpenAlexW2964806919MaRDI QIDQ2280212
Publication date: 18 December 2019
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00165-019-00490-3
softwareverificationreflectiontheorem provingrewritinginductionfunctional programmingdecision procedureshardwareLisp
History of computer science (68-03) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
- An extension of the Boyer-Moore theorem prover to support first-order quantification
- The addition of bounded quantification and partial functions to a computational logic and its theorem prover
- Prolegomena to a theory of mechanized formal reasoning
- Isabelle/HOL. A proof assistant for higher-order logic
- Efficient, verified checking of propositional proofs
- A man-machine theorem-proving system
- Limited second-order functionality in a first-order setting
- Efficient certified RAT verification
- Splitting and reduction heuristics in automatic theorem proving
- Linear resolution with selection function
- The ACL2 Sedan Theorem Proving System
- A fast string searching algorithm
- Toward Mechanical Mathematics
- Simplification by Cooperating Decision Procedures
- A Practical Decision Procedure for Arithmetic with Function Symbols
- Proving Theorems about LISP Functions
- A Machine-Oriented Logic Based on the Resolution Principle
- Automated Deduction – CADE-19
