Now showing items 1-9 of 9
Case-Analysis for Rippling and Inductive Proof
Rippling is a heuristic used to guide rewriting and is typically used for inductive theorem proving. We introduce a method to support case-analysis within rippling. Like earlier work, this allows goals containing if-statements ...
A Single-Significant-Digit Calculus for Semi-Automated Guesstimation
We describe a single-significant-digit calculus for estimating approximate solutions to guesstimation problems. The calculus is formalised as a collection of proof methods, which are combined into proof plans. These proof ...
Formalising Term Synthesis for Isacosy
IsaCoSy is a theory formation system for inductive theories. It synthesises conjectures and uses the ones that can be proved to produce a background theory for a new formalisation within a proof assistant. We present a ...
Scheme-Based Synthesis of Inductive Theories
We describe an approach to automatically invent/explore new mathematical theories, with the goal of producing results comparable to those produced by humans, as represented, for example, in the libraries of the Isabelle ...
Conjecture Synthesis for Inductive Theories
We have developed a program for inductive theory formation, called IsaCoSy, which synthesises conjectures ‘bottom-up’ from the available constants and free variables. The synthesis process is made tractable by only generating ...
Qualitative Causal Analysis of Empirical Knowledge for Ontology Evolution in Physics
Ontology evolution and its automation are key factors for achieving software’s ﬂexibility and adaptability. In the approach to automated ontology evolution adopted in the GALILEO project, progress in physics is modelled ...
Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery
We present a succinct account of dynamic rippling, a technique used to guide the automation of inductive proofs. This simplifies termination proofs for rippling and hence facilitates extending the technique in ways that ...
A Small Experiement in Event-b Rippling