Towards the animation of proofs -- testing proofs by examples

DOI10.1016/S0304-3975(00)00350-9zbMath0984.68138MaRDI QIDQ5958295

Ryosuke Sumitomo, Ken-ichiro Shii, Susumu Hayashi

Publication date: 3 March 2002

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

zbMATH Keywords

Curry-Howard isomorphismformal proof developmentstesting and debugging

Mathematics Subject Classification ID

Related Items (5)

Realizability interpretation of PA by iterated limiting PCA ⋮ Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1 ⋮ Program Testing and the Meaning Explanations of Intuitionistic Type Theory ⋮ Tool Support for Proof Engineering ⋮ Mathematics based on incremental learning -- excluded middle and inductive inference

Uses Software

• llprover

Cites Work

• The notion of proof in hardware verification
• Metamathematics, Machines and Gödel's Proof
• A new deconstructive logic: linear logic
• Pruning simply typed  -terms
• From programming-by-example to proving-by-example
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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