Now showing items 1-10 of 60
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 ...
Cooperating Reasoning Processes: More than Just the Sum of their Parts
(IJCAI Inc, 2007-01-06)
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 ...
Case-Analysis for Rippling and Inductive Proof
Rippling is a heuristic used to guide rewriting and is typically used for inductive theorem proving. We introduce a method to support case-analysis within rippling. Like earlier work, this allows goals containing if-statements ...
On Process Equivalence = Equation Solving in CCS
Unique Fixpoint Induction (UFI) is the chief inference rule to prove the equivalence of recursive processes in the Calculus of Communicating Systems (CCS) (Milner 1989). It plays a major role in the equational approach to ...
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 ...