## Search

Now showing items 31-40 of 60

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

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

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

#### Incidence Calculus

(John Wiley & Sons, 1992)

We describe incidence calculus, a logic for probabilistic reasoning. In incidence
calculus, probabilities are not directly associated with formulae. Rather
sets of possible worlds are directly associated with formulae ...

#### A general technique for automatically optimizing programs through the use of proof plans (Extended Abstract)

(Springer-Verlag, 1993)

The use of proof plans -formal patterns of reasoning for theorem
proving -to control the {automatic) synthesis of efficient programs from standard
definitional equations is described. A general framework for synthesizing ...

#### Correctness criteria of some algorithms for uncertain reasoning using Incidence Calculus

(SpringerLink, 1986-06)

Incidence Calculus is a technique for associating uncertainty values with logical sentences. These uncertainty values are called incidences and they are sets of points, which may be thought of as representing equivalence ...

#### Experiments in Automating Hardware Verification using Inductive Proof Planning

(Springer-Verlag, 1996)

We present a new approach to automating the verification of hardware designs based on planning techniques. A database of methods is developed that combines tactics, which construct proofs, using specifications of their ...

#### Proof Plans for the Correction of False Conjectures

(Springer Verlag, 1994)

Theorem proving is the systematic derivation of a mathcmaticM
proof from a set of axioms by the use of rules of inference. We ~re
interested in a related but far less explored problem: the analysis and
correction of ...