## Search

Now showing items 31-40 of 60

#### Special Purpose, but Domain Independent, Inference Mechanisms

(1987)

vie describe a number of special purpose, but domain independent, inference mechanisms.
While these rl1echanisms are limited to certain kinds of inference and
illference rules, they do not rely ...

#### Automation of Diagrammatic Reasoning

(Morgan Kaufmann, 1997)

Theorems in automated theorem proving are usually proved by logical formal proofs. However, there is a subset of problems which humans can prove in a different way by the use of geometric operations on diagrams, so called ...

#### Increasing the Versatility of Heuristic Based Theorem Provers

(Springer Verlag, 1993)

Heuristic based theorem proving systems typically impose a fixed ordering on the strategies which they embody. The ordering reflects the general experience of the system designer. As a consequence, there will exist a variety ...

#### Plan Execution Failure Analysis Using Plan Deconstruction

(2003-12)

We consider the challenges that arise when plans are based on an incorrect representation of the domain in which they are executed. We describe how information about plan formation, and how the way in which each plan step ...

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

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

#### The Use of Explicit Plans to Guide Inductive Proofs

(SpringerLink, 1988-05)

We propose the use of explicit proof plans to guide the search for a proof in automatic theorem proving. By representing proof plans as the specifications of LCF-like tactics, [Gordon et al 79], and by recording these ...

#### Rippling: A Heuristic for Guiding Inductive Proofs

(Elsevier, 1993-08)

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

#### Attacking the Asokan-Ginzboorg Protocol for Key Distribution in an Ad-Hoc Bluetooth Network Using CORAL

(2003-10)

We describe Coral, a counterexample finder for incorrect inductive conjectures. By devising a first-order version of Paulson's formalism for cryptographic protocol analysis, we are able to use Coral to attack protocols ...