Towards the animation of proofs -- testing proofs by examples

DOI10.1016/S0304-3975(00)00350-9MaRDI QIDQ5958295zbMATH OpenFDO

Authors Susumu Hayashi, Ryosuke Sumitomo, Ken-ichiro Shii

Publication date 3 March 2002

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S0304-3975(00)00350-9

zbMATH Keywords

Curry-Howard isomorphismformal proof developmentstesting and debugging

Mathematics Subject Classification ID

Recommendations

• scientific article; zbMATH DE number 2086734
• Proviola: a tool for proof re-animation
• From programming-by-example to proving-by-example
• ProofViz: an interactive visual proof explorer

Cites work

• A new deconstructive logic: linear logic
• From programming-by-example to proving-by-example
• scientific article; zbMATH DE number 1222086 (Why is no real title available?)
• scientific article; zbMATH DE number 1302054 (Why is no real title available?)
• scientific article; zbMATH DE number 1302630 (Why is no real title available?)
• scientific article; zbMATH DE number 1324438 (Why is no real title available?)
• scientific article; zbMATH DE number 715447 (Why is no real title available?)
• Metamathematics, Machines and Gödel's Proof
• Pruning simply typed  -terms
• The notion of proof in hardware verification

Cited in

(10)

• Tool support for proof engineering
• Proviola: a tool for proof re-animation
• Can proofs be animated by games?
• Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1
• Jape: a calculator for animating proof-on-paper
• Program testing and the meaning explanations of intuitionistic type theory
• Typed Lambda Calculi and Applications
• Computer Algebra and Geometric Algebra with Applications
• Realizability interpretation of PA by iterated limiting PCA
• Mathematics based on incremental learning -- excluded middle and inductive inference

Describes a project that uses

Uses Software

• llprover

This page was built for publication: Towards the animation of proofs -- testing proofs by examples

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