An lCF-style interface between HOL and first-order logic

DOI10.1007/3-540-45620-1_10MaRDI QIDQ4809048zbMATH OpenFDO

Authors Joe Hurd

Publication date 12 August 2004

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2392/23920134.htm

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• From LCF to Isabelle/HOL
• Twenty Years of Theorem Proving for HOLs Past, Present and Future
• Automatic proof and disproof in Isabelle/HOL
• Automation for interactive proof: first prototype
• scientific article; zbMATH DE number 234014

Cited in

(18)

• Integrating external deduction tools with ACL2
• Efficiently checking propositional refutations in HOL theorem provers
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Translating higher-order clauses to first-order clauses
• Mark Stickel: his earliest work
• Implicational rewriting tactics in HOL
• scientific article; zbMATH DE number 2185697 (Why is no real title available?)
• Validating QBF Validity in HOL4
• Proving Valid Quantified Boolean Formulas in HOL Light
• Expressing polymorphic types in a many-sorted language
• Superposition for lambda-free higher-order logic
• The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4
• Using First-Order Theorem Provers in the Jahob Data Structure Verification System
• Frontiers of Combining Systems
• A Mizar mode for HOL
• Hammering higher order set theory
• Types, Tableaus and Gödel’s God in Isabelle/HOL
• Combined reasoning by automated cooperation

Describes a project that uses

Uses Software

• HOL

This page was built for publication: An lCF-style interface between HOL and first-order logic

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