Theorem Proving in Higher Order Logics

DOI10.1007/B100400MaRDI QIDQ5464665zbMATH OpenOpenAlexFDO

Authors Ruben A. Gamboa, John Cowles

Publication date 18 August 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b100400

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Recommendations

• Church meets Cook and Levin
• Proof pearl: proving a simple von Neumann machine Turing complete
• The complexity of satisfiability problems
• Proving completeness by logic
• scientific article; zbMATH DE number 1179974

Cited in

(3)

• Proof pearl: proving a simple von Neumann machine Turing complete
• Church meets Cook and Levin
• A mechanized proof of the basic perturbation lemma

Describes a project that uses

Uses Software

• ACL2

This page was built for publication: Theorem Proving in Higher Order Logics

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