Interactive theorem proving. Preface of the special issue

DOI10.1007/S10817-016-9363-7zbMATH Open1336.00112OpenAlexW2284603212MaRDI QIDQ287356FDOQ287356

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

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.

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)

Cited In (5)

• Collaborative Interactive Theorem Proving with Clide
• Title not available (Why is that?)
• 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

Uses Software

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

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)