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 λ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.

• Type: Conference
• Year: 1999
• Where: LPAR
• Authors: Alan Bundy, Julian Richardson
• Keywords: Automated Reasoning, Elliptic Formulae, Formal Proofs, LPAR 1999, λClam Proof Planner