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 ...
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 ...
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 ...
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 ...