Now showing items 1-10 of 10
Cross Domain Mathematical Concept Formation
(The University of Edinburgh, 2000)
Many interesting concepts in mathematics are essentially "cross-domain" in nature, relating objects from more than one area of mathematics, e.g. prime order groups. These concepts are often vital to the formation of a ...
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 ...
Plan Execution Failure Analysis Using Plan Deconstruction
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 ...
Attacking the Asokan-Ginzboorg Protocol for Key Distribution in an Ad-Hoc Bluetooth Network Using CORAL
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 ...
Diagnosing and Repairing Ontological Mismatches
The development of the semantic web ensures that the facilitation of agent communication is an issue of increasing importance. It is usually assumed that agents are using the same ontology and hence can understand one ...
An Automatic Translator from KIF to PDDL
In this paper, we present a translation process that we have developed to convert KIF ontologies into PDDL. This allows us to define KIF-based agents that can plan efficiently. We discuss the difficulties inherent in ...
Isacosy: Synthesis of Inductive Theorems
We have implemented a program for inductive theory formation, called IsaCoSy, which synthesises conjectures about recursively deﬁned datatypes and functions. Only irreducible terms are generated, which keeps the search ...
Veriﬁed Planning by Deductive Synthesis in Intuitionistic Linear Logic
We describe a new formalisation in Isabelle/HOL of Intuitionistic Linear Logic and consider the support this provides for constructing plans by proving the achievability of given planning goals. The plans so found are ...