## Search

Now showing items 1-9 of 9

#### Case-Analysis for Rippling and Inductive Proof

(Springer, 2010)

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

(SpringerLink, 2010)

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

(2010)

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

(2010)

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

(SpringerLink, 2010)

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

(2010-08-16)

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

(Springer-Verlag, 2010)

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

(2011-02-03)