Proofs About Lists Using Ellipsis

Alan Bundy, Julian Richardson

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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.
Original languageEnglish
Title of host publicationLogic for Programming and Automated Reasoning
Subtitle of host publication6th International Conference, LPAR’99 Tbilisi, Georgia, September 6–10, 1999 Proceedings
EditorsHarald Ganzinger, David McAllester, Andrei Voronkov
PublisherSpringer-Verlag GmbH
Number of pages12
ISBN (Electronic)978-3-540-48242-0
ISBN (Print)978-3-540-66492-5
Publication statusPublished - 1999

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Cite this