Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

10

LPAR
1999
Springer

favoriteEmaildiscussreport

81views Automated Reasoning» more LPAR 1999»

Proofs About Lists Using Ellipsis

13 years 9 months ago

Proofs About Lists Using Ellipsis

Download www.inf.ed.ac.uk

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 λClam proof planner. We use an unambiguous higher-order formulation of lists which is amenable to formal proofs without using induction, and to display using the familiar ... notation.

Alan Bundy, Julian Richardson

Real-time Traffic

Automated Reasoning | Elliptic Formulae | Formal Proofs | LPAR 1999 | λClam Proof Planner |

claim paper

Related Content

» Proving Properties about Lists Using Containers

» Constructing List Homomorphisms from Proofs

» Reasoning about B Trees with Operational Semantics and Separation Logic

» Induction and Coinduction in Sequent Calculus

» Cyclic proofs of program termination in separation logic

» Formal verification of translation validators a case study on instruction scheduling optim...

» Verifiable Rotation of Homomorphic Encryptions

» Certified assembly programming with embedded code pointers

» A Practical System for Globally Revoking the Unlinkable Pseudonyms of Unknown Users

Post Info
More Details (n/a)

Added	04 Aug 2010
Updated	04 Aug 2010
Type	Conference
Year	1999
Where	LPAR
Authors	Alan Bundy, Julian Richardson

Comments (0)