Now showing items 1-10 of 24
Proofs About Lists Using Ellipsis
In this paper we explore the use of ellipsis in proofs about lists. We present a higher-order formulation of elliptic formulae, and describe its implementation in the LambdaClam proof planner. We use an unambiguous ...
Making a Productive Use of Failure to Generate Witnesses for Coinduction from Divergent Proof Attempts
Coinduction is a proof rule. It is the dual of induction. It allows reasoning about non--well--founded structures such as lazy lists or streams and is of particular use for reasoning about equivalences. A central difficulty ...
A Survey of Automated Deduction
We survey research in the automation of deductive inference, from its beginnings in the early history of computing to the present day. We identify and describe the major areas of research interest and their applications. ...
The Automation Of Proof By Mathematical Induction
This paper is a chapter of the Handbook of Automated Reasoning edited by Voronkov and Robinson. It describes techniques for automated reasoning in theories containing rules of mathematical induction. Firstly, inductive ...
`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 ...
Automatic Concept Formation in Pure Mathematics
The HR program forms concepts and makes conjectures in domains of pure mathematics and uses theorem prover OTTER and model generator MACE to prove or disprove the conjectures. HR measures properties of concepts and assesses ...
The New Software Copyright Law
(Oxford University Press, 1994-03)
Turning Eureka Steps into Calculations in Automatic Program Synthesis
A description is given of a technique called middle-out reasoning for the control of search in automatic theorem proving. The authors illustrate it use in the domain of automatic program synthesis. Programs can be synthesised ...