Experiments with proof plans for induction

DOI10.1007/BF00249016zbMath0733.68069OpenAlexW2034500240WikidataQ56840274 ScholiaQ56840274MaRDI QIDQ809617

Frank van Harmelen, Alan Bundy, Alan Smaill, Jane Hesketh

Publication date: 1991

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00249016

zbMATH Keywords

theorem provingplanningmathematical inductionprogram synthesistacticsSearchingcombinatorial explosionproof plans

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items

On process equivalence = equation solving in CCS ⋮ Proof planning with multiple strategies ⋮ An integrated approach to high integrity software verification ⋮ A calculus for and termination of rippling ⋮ Conjecture synthesis for inductive theories ⋮ Knowledge-based proof planning ⋮ Internal analogy in theorem proving ⋮ Rippling: A heuristic for guiding inductive proofs ⋮ Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery ⋮ Discussing Hilbert's 24th problem ⋮ Lazy techniques for fully expansive theorem proving

Uses Software

• Isabelle
• Nuprl
• CLAM
• Oyster

Cites Work

• Edinburgh LCF. A mechanized logic of computation
• Planning in a hierarchy of abstraction spaces
• A Transformation System for Developing Recursive Programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item