Now showing items 51-60 of 60
Correctness criteria of some algorithms for uncertain reasoning using Incidence Calculus
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
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 ...
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 ...
Constructing Probabilistic ATMS Using Extended Incidence Calculus
This paper discusses the relations between extended incidence calculus and assumption-based truth maintenance systems (ATMSs). We first prove that managing labels for statements (nodes) in an ATMS is equivalent to producing ...
The Use of Proof Plans to Sum Series
(Springer Verlag, 1992)
We describe a program for finding closed form solutions to finite sums. The program was built to test the applicability of the proof planning search control technique in a domain of mathematics outwith induction. This ...
Dynamic Rippling, Middle-Out Reasoning and Lemma Discovery
We present a succinct account of dynamic rippling, a technique used to guide the automation of inductive proofs. This simplifies termination proofs for rippling and hence facilitates extending the technique in ways that ...
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 ...
A Small Experiement in Event-b Rippling
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 ...