A theorem prover for a computational logic
From MaRDI portal
Publication:6488518
DOI10.1007/3-540-52885-7_75zbMath1509.68296MaRDI QIDQ6488518
J. Strother Moore, Robert S. Boyer
Publication date: 28 April 2023
Recursive functions and relations, subrecursive hierarchies (03D20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (3)
Induction using term orders ⋮ Fermat, Euler, Wilson -- three case studies in number theory ⋮ Combining induction and saturation-based theorem proving
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
- Unnamed Item
- Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm
- Computer proofs in group theory
- The addition of bounded quantification and partial functions to a computational logic and its theorem prover
- A mechanical proof of the termination of Takeuchi's function
- An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem
- On the role of automated theorem proving in the compile-time derivation of concurrency
- Towards mechanical metamathematics
- The automated proof of a trace transformation for a bitonic sort
- Splitting and reduction heuristics in automatic theorem proving
- Computer proofs of limit theorems
- Recursive functions of symbolic expressions and their computation by machine, Part I
- Proof Checking the RSA Public Key Encryption Algorithm
- A Mechanical Proof of the Unsolvability of the Halting Problem
- A mechanical proof of the Church-Rosser theorem
- Reaching Agreement in the Presence of Faults
- The Byzantine Generals Problem
- Proving Theorems about LISP Functions
- A Machine-Oriented Logic Based on the Resolution Principle
- The Concept of Demodulation in Theorem Proving
- Proving Properties of Programs by Structural Induction
- An axiomatic basis for computer programming
This page was built for publication: A theorem prover for a computational logic
