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 ...
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 ...
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. ...
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 ...
Automation of Diagrammatic Reasoning
(Morgan Kaufmann, 1997)
Theorems in automated theorem proving are usually proved by logical formal proofs. However, there is a subset of problems which humans can prove in a different way by the use of geometric operations on diagrams, so called ...
Increasing the Versatility of Heuristic Based Theorem Provers
(Springer Verlag, 1993)
Heuristic based theorem proving systems typically impose a fixed ordering on the strategies which they embody. The ordering reflects the general experience of the system designer. As a consequence, there will exist a variety ...
`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 ...
Extensions to the Rippling-Out Tactic for Guiding Inductive Proofs
(Springer Verlag, 1990)
In earlier papers we described a technique for automatically constructing inductive proofs, using a heuristic search control tactic called rippling-out. Further testing on harder examples has shown that the rippling-out ...