An Isabelle-like procedural mode for HOL Light

DOI10.1007/978-3-642-16242-8_40MaRDI QIDQ4933332zbMATH OpenOpenAlexFDO

Authors Petros Papapanagiotou, Jacques D. Fleuriot

Publication date 12 October 2010

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-16242-8_40

Mathematics Subject Classification ID

Recommendations

• HOL Light: An Overview
• Equational reasoning in Isabelle
• Automated Reasoning
• Formalization of linear space theory in the higher-order logic proving system
• The Lean theorem prover (system description)

Cited in

(5)

• Equational reasoning in Isabelle
• Lemma Mining over HOL Light
• Importing HOL Light into Coq
• Re-imagining the Isabelle archive of formal proofs
• Object-level reasoning with logics encoded in HOL Light

Describes a project that uses

Uses Software

• Coq
• HOL Light
• Isabelle

This page was built for publication: An Isabelle-like procedural mode for HOL Light

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