Click'n prove: interactive proofs within set theory

DOI10.1007/10930755_1MaRDI QIDQ3559759zbMATH OpenOpenAlexFDO

Authors Dominique Cansell, Jean-Raymond Abrial

Publication date 7 May 2010

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

Full work available at URL https://doi.org/10.1007/10930755_1

Mathematics Subject Classification ID

Set theory (03E99)

Recommendations

• ProofViz: an interactive visual proof explorer
• scientific article; zbMATH DE number 1629953
• An Interactive Driver for Goal-directed Proof Strategies
• scientific article; zbMATH DE number 2154392
• scientific article; zbMATH DE number 4072441

Cited in

(7)

• The RISC ProofNavigator: a proving assistant for program verification in the classroom
• Proving pointer programs in higher-order logic
• Some considerations on the usability of interactive provers
• scientific article; zbMATH DE number 1479613 (Why is no real title available?)
• Incremental parametric development of greedy algorithms
• Verified Compilation and the B Method: A Proposal and a First Appraisal
• Formal and incremental construction of distributed algorithms: on the distributed reference counting algorithm

Describes a project that uses

Uses Software

• Coq
• Isabelle
• OTTER
• Proof General

This page was built for publication: Click'n prove: interactive proofs within set theory

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