## Search

Now showing items 1-10 of 60

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

#### A Subsumption Architecture for Theorem Proving?

(The Royal Society, 1994-10)

Brooks has criticized traditional approaches
to artificial
intelligence as too ineffi-
cient. In particular, he has singled out techniques involving
search as
inadequate
to achieve the fast reaction times ...

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

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

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

#### Intelligent Front Ends

(1984)

An intelligent front end is a user-friendly interface to a software package, which
uses Artificial Intelligence techniques to enable the user to interact with the computer
using his/her own terminology rather than that ...

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

#### Incidence Calculus: A Mechanism for Probabilistic Reasoning

(D. Reidet Publishing Company, 1985)

Mechanisms for the automation of uncertainty are required for expert systems. Sometimes these
mechanisms need to obey the properties of probabilistic reasoning. We argue that a purely numeric
mechanism, ...

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