Now showing items 1-4 of 4
Turning Eureka Steps into Calculations in Automatic Program Synthesis
A description is given of a technique called middle-out reasoning for the control of search in automatic theorem proving. The authors illustrate it use in the domain of automatic program synthesis. Programs can be synthesised ...
Rippling: A Heuristic for Guiding Inductive Proofs
We describe rippling: a tactic for the heuristic control of the key part of proofs by mathematical induction. This tactic significantly reduces the search for a proof of a wide variety of inductive theorems. We first present ...
Extensions to the Rippling-Out Tactic for Guiding Inductive Proofs
(Springer Verlag, 1990)
In earlier papers we described a technique for automatically constructing inductive proofs, using a heuristic search control tactic called rippling-out. Further testing on harder examples has shown that the rippling-out ...
Veriﬁed Planning by Deductive Synthesis in Intuitionistic Linear Logic
We describe a new formalisation in Isabelle/HOL of Intuitionistic Linear Logic and consider the support this provides for constructing plans by proving the achievability of given planning goals. The plans so found are ...