Now showing items 1-10 of 55
Cooperating Reasoning Processes: More than Just the Sum of their Parts
(IJCAI Inc, 2007-01-06)
On Process Equivalence = Equation Solving in CCS
Unique Fixpoint Induction (UFI) is the chief inference rule to prove the equivalence of recursive processes in the Calculus of Communicating Systems (CCS) (Milner 1989). It plays a major role in the equational approach to ...
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 Generalized Interval Package and its Use for Semantic Checking
(Transactions on Mathematical Software, 1984-12)
`Semantic procedure' is an oxymoron
(Cambridge University Press, 1993)
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 ...
A Recursive Techniques Editor for Prolog
We describe an editor geared to recursive Prolog procedures. It is similar to the structure editors built for many programming languages, except that instead of just ensuring the correctness of the syntax of the procedures ...
Raising the Standard of AI Products
We propose a mechanism for the promotion of high-standards in commercial Artificial Intelligence products, namely an association of companies which would regulate their own membership using a code of practice and the ...
Solving Mechanics Problems Using Meta-Level Inference
In this paper we shall describe a program (MECHO), written in Prolog, which solves a wide range of mechanics problems from statements in both predicate calculus and English. Mecho uses the technique of meta-level ...