TY - GEN
T1 - Proofs About Lists Using Ellipsis
AU - Bundy, Alan
AU - Richardson, Julian
PY - 1999
Y1 - 1999
N2 - 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.
AB - 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.
U2 - 10.1007/3-540-48242-3_1
DO - 10.1007/3-540-48242-3_1
M3 - Conference contribution
SN - 978-3-540-66492-5
T3 - Lecture Notes in Computer Science
SP - 1
EP - 12
BT - Logic for Programming and Automated Reasoning
A2 - Ganzinger, Harald
A2 - McAllester, David
A2 - Voronkov, Andrei
PB - Springer-Verlag GmbH
ER -