Now showing items 51-60 of 60
What Is The Well-Dressed AI Educator Wearing Now?
A funny thing happened to me at IJCAI-81. I went to a panel on "Education in AI" and stepped back into an argument that I had thought settled several years ago. The debate was between the "scruffies," led by Roger Schank ...
The New Software Copyright Law
(Oxford University Press, 1994-03)
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 ...
Scheme-Based Synthesis of Inductive Theories
We describe an approach to automatically invent/explore new mathematical theories, with the goal of producing results comparable to those produced by humans, as represented, for example, in the libraries of the Isabelle ...
The Use of Prolog for Improving the Rigour and Accessibility of Ecological Modelling
We introduce three concepts that offer considerable benefit to the process of ecological modelling: the descriptive representation of models; the explicit representation of knowledge about how to model; and the development ...
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 ...
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 ...
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 ...
A Small Experiement in Event-b Rippling