Middle-out reasoning for synthesis and induction
type: Item
instance of: scholarly article
title: Middle-out reasoning for synthesis and induction
zbMATH Open document ID: 0847.68104
DOI: 10.1007/BF00244461
author: Ina Kraan
author: Alan Bundy
author: David Basin
published in: Journal of Automated Reasoning
publication date: 1996-06-11T00:00:00Z
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 887166
zbMATH Keywords: middle-out reasoning
zbMATH Keywords: logic program synthesis
zbMATH Keywords: induction schemes
describes a project that uses: NQTHM
describes a project that uses: Oyster
describes a project that uses: InKa
describes a project that uses: CLAM
describes a project that uses: Mollusc
MaRDI profile type: Publication
cites work: Mechanizing structural induction. II: Strategies
cites work: Q4023948
cites work: Q4040283
cites work: Q3804239
cites work: Rippling: A heuristic for guiding inductive proofs
cites work: Q3490990
cites work: Q4138099
cites work: Logic program synthesis
cites work: Q3743300
cites work: Edinburgh LCF. A mechanized logic of computation
cites work: A unification algorithm for typed \(\bar\lambda\)-calculus
cites work: Synthesis of induction orderings for existence proofs
cites work: Productive use of failure in inductive proof
cites work: Q3992908
cites work: Q3328540
cites work: A logic programming language with lambda-abstraction, function variables, and simple unification
cites work: Lazy generation of induction hypotheses
cites work: Mollusc a general proof-development shell for sequent-based logics
cites work: The OYSTER-CLAM system
description: scientific article; zbMATH DE number 887166