scientific article; zbMATH DE number 3880145

MaRDI QIDQ3345811zbMATH OpenFDO

Authors Robert S. Boyer, J Strother Moore

Publication date 1984

zbMATH Keywords

Fermat's theoremheuristicsrecursive unsolvability of the halting problemuniqueness of prime factorizationsverification condition generator

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Symbolic computation and algebraic computation (68W30)

Recommendations

• scientific article; zbMATH DE number 1360950
• A theorem prover for a computational logic
• scientific article; zbMATH DE number 13446
• Simplify: a theorem prover for program checking
• Computer theorem proving in mathematics

Cited in

(40)

• A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
• Computer programs and mathematical proofs
• The problem of induction
• Abstract proof checking: An example motivated by an incompleteness theorem
• Using the VIRT programming language for automatic theorem proving
• An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem
• Towards mechanical metamathematics
• An interactive calculus theorem-prover for continuity properties
• A fully automatic theorem prover with human-style output
• Proof checking and logic programming
• How to avoid the formal verification of a theorem prover
• Theorem proving method and the computer science
• Poitín: distilling theorems from conjectures
• scientific article; zbMATH DE number 5917352 (Why is no real title available?)
• scientific article; zbMATH DE number 2177632 (Why is no real title available?)
• scientific article; zbMATH DE number 3858384 (Why is no real title available?)
• scientific article; zbMATH DE number 4201687 (Why is no real title available?)
• System of automation of proving theorems of the theory of metanominative data
• scientific article; zbMATH DE number 4164171 (Why is no real title available?)
• Simplify: a theorem prover for program checking
• Machine Checking Proof Theory: An Application of Logic to Logic
• Proofs verifying programs and programs producing proofs: a conceptual analysis
• scientific article; zbMATH DE number 3904000 (Why is no real title available?)
• Lessons learned from LCF: A Survey of Natural Deduction Proofs
• scientific article; zbMATH DE number 3938594 (Why is no real title available?)
• A Mechanical Proof of the Unsolvability of the Halting Problem
• scientific article; zbMATH DE number 4074537 (Why is no real title available?)
• scientific article; zbMATH DE number 4092761 (Why is no real title available?)
• scientific article; zbMATH DE number 13446 (Why is no real title available?)
• scientific article; zbMATH DE number 1360950 (Why is no real title available?)
• scientific article; zbMATH DE number 549074 (Why is no real title available?)
• scientific article; zbMATH DE number 1088222 (Why is no real title available?)
• A nucleus of a theorem-prover described inAlgol-68
• scientific article; zbMATH DE number 1507199 (Why is no real title available?)
• scientific article; zbMATH DE number 1538014 (Why is no real title available?)
• Proof verification and proof discovery for relativity
• Computer Aided Verification
• An automatic proof of Gödel's incompleteness theorem
• Automated theorem provers: a practical tool for the working mathematician?
• Computer theorem proving in mathematics

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3345811)