Some considerations on the usability of interactive provers

DOI10.1007/978-3-642-14128-7_13MaRDI QIDQ3582703zbMATH OpenOpenAlexFDO

Authors Andrea Asperti, Claudio Sacerdoti Coen

Publication date 24 August 2010

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-14128-7_13

Mathematics Subject Classification ID

Recommendations

• scientific article; zbMATH DE number 3870635
• Click'n prove: interactive proofs within set theory
• Publication:3034850
• Automated theorem provers: a practical tool for the working mathematician?
• Automated Reasoning

Cited in

(8)

• Theorem proving in technology transfer: The user's point of view
• Theory presentation combinators
• scientific article; zbMATH DE number 4133524 (Why is no real title available?)
• scientific article; zbMATH DE number 1857499 (Why is no real title available?)
• Pollack-inconsistency
• Isabelle formalisation of original representation theorems
• O₂ is a multiple context-free grammar: an implementation-, formalisation-friendly proof
• A formalization of multi-tape Turing machines

Describes a project that uses

Uses Software

• Nuprl
• LCF

This page was built for publication: Some considerations on the usability of interactive provers

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