scientific article; zbMATH DE number 1479613

MaRDI QIDQ4490725zbMATH OpenFDO

Authors Yves Bertot, G. Kahn, Laurent Théry

Publication date 20 July 2000

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 2090059
• Click'n prove: interactive proofs within set theory
• scientific article; zbMATH DE number 3922016
• scientific article; zbMATH DE number 1629953
• Visual theorem proving with the Incredible Proof Machine

Cited in

(9)

• Subformula linking for intuitionistic logic with application to type theory
• User interaction with the Matita proof assistant
• Coqpie: an IDE aimed at improving proof development productivity (rough diamond)
• scientific article; zbMATH DE number 2090059 (Why is no real title available?)
• Encoding natural semantics in Coq
• A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs
• Jape: a calculator for animating proof-on-paper
• A living monograph for graph transformation
• The flower calculus

This page was built for publication:

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