Productive use of failure in inductive proof
From MaRDI portal
Publication:1915134
DOI10.1007/BF00244460zbMath0847.68103MaRDI QIDQ1915134
Publication date: 11 June 1996
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Related Items
An integrated approach to high integrity software verification, \textit{Theorema}: Towards computer-aided mathematical theory exploration, A proof-centric approach to mathematical assistants, Supporting the formal verification of mathematical texts, Proof-search in type-theoretic languages: An introduction, Appropriate lemmae discovery, On terminating lemma speculations., Middle-out reasoning for synthesis and induction, A calculus for and termination of rippling, Proving theorems by reuse
Uses Software
Cites Work