Now showing items 1-5 of 5
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 ...
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 ...