Productive use of failure in inductive proof
type: Item
instance of: scholarly article
title: Productive use of failure in inductive proof
zbMATH Open document ID: 0847.68103
DOI: 10.1007/BF00244460
author: Andrew Ireland
author: Alan Bundy
published in: Journal of Automated Reasoning
publication date: 1996-06-11T00:00:00Z
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 887165
zbMATH Keywords: mathematical induction
zbMATH Keywords: rippling
zbMATH Keywords: inductive reasoning
describes a project that uses: CLAM
describes a project that uses: LCF
describes a project that uses: Oyster
MaRDI profile type: Publication
cites work: Q3894958
cites work: Implicit induction in conditional theories
cites work: Rippling: A heuristic for guiding inductive proofs
cites work: Q3804239
cites work: Q4264732
cites work: Q5610986
cites work: Edinburgh LCF. A mechanized logic of computation
cites work: A colored version of the λ-calculus
cites work: Q3690194
cites work: A divergence critic
cites work: The OYSTER-CLAM system
cites work: Extensions to the rippling-out tactic for guiding inductive proofs
cites work: Guiding induction proofs
full work available at URL: https://doi.org/10.1007/bf00244460
OpenAlex ID: W2067540169
Recommended article: Predicting Failures of and Repairing Inductive Proof Attempts
Recommended article: Making a productive use of failure to generate witnesses for coinduction from divergent proof attempts
Recommended article: Logic Based Program Synthesis and Transformation
Recommended article: A proof theoretic approach to failure in functional logic programming
Recommended article: Q2767053
Recommended article: Failure reasoning in multiple-strategy proof planning
Recommended article: Q3804239
Recommended article: Strictness analysis aids inductive proofs
Recommended article: Induction on Failure: Learning Connected Horn Theories
description: scientific article; zbMATH DE number 887165