Edinburgh Research Explorer

Proofs About Lists Using Ellipsis

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

Related Edinburgh Organisations

Documents

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
Pages1-12
Number of pages12
ISBN (Electronic)978-3-540-48242-0
ISBN (Print)978-3-540-66492-5
DOIs
StatePublished - 1999

Publication series

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

Abstract

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.

Download statistics

No data available

ID: 7543178