Interactive theorem proving. Preface of the special issue

DOI10.1007/S10817-016-9363-7MaRDI QIDQ287356zbMATH OpenOpenAlexFDO

Authors

Publication date 26 May 2016

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-016-9363-7

zbMATH Keywords

formal logicformal verificationinteractive theorem proving

Mathematics Subject Classification ID

Collections of articles of miscellaneous specific interest (00B15) Proceedings, conferences, collections, etc. pertaining to computer science (68-06)

Recommendations

• Preface to the special issue: Interactive theorem proving and the formalization of mathematics
• Foreword to: Special issue on interactive theorem provers
• A survey of interactive theorem proving
• scientific article; zbMATH DE number 3870635
• Interactive theorem proving from the perspective of Isabelle/Isar
• A synthesis of the procedural and declarative styles of interactive theorem proving
• Partiality and recursion in interactive theorem provers -- an overview
• Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0
• Embedding complex decision procedures inside an interactive theorem prover.

Cited in

(5)

• 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)
• Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem
• Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0

Describes a project that uses

Uses Software

• Eisbach
• Coq/SSReflect
• HOL
• Isabelle/HOL
• Isabelle
• Coq

This page was built for publication: Interactive theorem proving. Preface of the special issue

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