Fundamental proof methods in computer science. A computer-based approach

MaRDI QIDQ5364939zbMATH OpenFDO

Authors Konstantine Arkoudas, David R. Musser

Publication date 29 September 2017

zbMATH Keywords

Athenacomputer sciencedenotational proof languagesmachine-checkable proofsproof methods

Mathematics Subject Classification ID

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Logic in computer science (03B70) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01)

Recommendations

• The little prover. With a foreword by J. Strother Moore. With an afterword by Matthias Felleisen
• scientific article; zbMATH DE number 3976991
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Computational logic and set theory. Applying formalized logic to analysis. Foreword by Martin Davis
• scientific article; zbMATH DE number 49488

Cited in

(8)

• Applied logic for computer scientists. Computational deduction and formal proofs
• Athena
• Structural proof theory. With an appendix by Aarne Ranta
• Theorem proving method and the computer science
• Logic and Computation
• Design patterns for mathematical proofs. A guide, in particular for computer scientists
• Essential logic for computer science
• The little prover. With a foreword by J. Strother Moore. With an afterword by Matthias Felleisen

This page was built for publication: Fundamental proof methods in computer science. A computer-based approach

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