A survey of interactive theorem proving

MaRDI QIDQ6173578zbMATH OpenFDO

Authors Filip Marić

Publication date 21 July 2023

Full work available at URL http://elib.mi.sanu.ac.rs/files/journals/zr/26/zrn26p173-223.pdf

zbMATH Keywords

formal logicinteractive theorem provingproof assistants

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Interactive theorem proving from the perspective of Isabelle/Isar
• An Interactive Driver for Goal-directed Proof Strategies
• Foreword to: Special issue on interactive theorem provers
• Pervasive parallelism in highly-trustable interactive theorem proving systems
• The Matita interactive theorem prover

Cited in

(10)

• Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem
• scientific article; zbMATH DE number 1629956 (Why is no real title available?)
• Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0
• Interactive theorem proving. Preface of the special issue
• Collaborative Interactive Theorem Proving with Clide
• scientific article; zbMATH DE number 3870635 (Why is no real title available?)
• The Abella Interactive Theorem Prover (System Description)
• scientific article; zbMATH DE number 1765687 (Why is no real title available?)
• An Interactive Driver for Goal-directed Proof Strategies
• Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points

This page was built for publication: A survey of interactive theorem proving

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