Interactive theorem proving from the perspective of Isabelle/Isar

MaRDI QIDQ5219926zbMATH OpenFDO

Authors Makarius Wenzel

Publication date 9 March 2020

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• From LCF to Isabelle/HOL
• The Isabelle Framework
• Interaction with formal mathematical documents in Isabelle/PIDE
• Isabelle as document-oriented proof assistant
• Automatic proof and disproof in Isabelle/HOL

Cited in

(24)

• Using the Isabelle ontology framework -- linking the formal with the informal
• Equational reasoning in Isabelle
• Verified interactive computation of definite integrals
• Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
• From LCF to Isabelle/HOL
• Interaction with formal mathematical documents in Isabelle/PIDE
• scientific article; zbMATH DE number 1629956 (Why is no real title available?)
• Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0
• Pervasive parallelism in highly-trustable interactive theorem proving systems
• Interactive theorem proving. Preface of the special issue
• On definitions of constants and types in HOL
• scientific article; zbMATH DE number 3870635 (Why is no real title available?)
• The Lean theorem prover (system description)
• The Abella Interactive Theorem Prover (System Description)
• Managing proof documents for asynchronous processing
• Isabelle as document-oriented proof assistant
• Integration of automated and interactive theorem proving in ILF
• Automated Reasoning
• Shared-memory multiprocessing for interactive theorem proving
• An approach to the extension of a theorem prover by advanced structuring mechanisms.
• A Framework for Interactive Proof
• Interactive simplifier tracing and debugging in Isabelle
• Structured Induction Proofs in Isabelle/Isar
• A survey of interactive theorem proving

Describes a project that uses

Uses Software

• ACL2
• Isabelle/HOL
• Metis
• Mizar
• Proof General
• LCF
• CakeML
• Nitpick
• Archive of Formal Proofs
• Coq
• Isabelle/Isar
• PVS
• z3
• HOL
• OCaml
• PIDE
• Isabelle/jEdit
• HOL Light
• Coq/SSReflect
• CompCert
• Flyspeck
• Isabelle
• Sledgehammer

This page was built for publication: Interactive theorem proving from the perspective of Isabelle/Isar

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