Proofs About Lists Using Ellipsis

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.

Authors

• Alan Bundy
• Julian Richardson

Keywords

No keywords are indexed for this paper.