@inproceedings{W13,
  Abstract =	 {We re-investigate a proof example presented by
                  George Boolos which perspicuously illustrates
                  G\"odel's argument for the potentially drastic
                  increase of proof-lengths in formal systems when
                  carrying through the argument at too low a
                  level. More concretely, restricting the order of the
                  logic in which the proof is carried through to the
                  order of the logic in which the problem is
                  formulated in the first place can result in
                  unmanageable long proofs, although there are short
                  proofs in a logic of higher order. Our motivation in
                  this paper is of practical nature and its aim is to
                  sketch the implications of this example to current
                  technology in automated theorem proving, to point to
                  related questions about the foundational character
                  of type theory (without explicit comprehension
                  axioms) for mathematics, and to work out some
                  challenging aspects with regard to the automation of
                  this proof -- which, as we belief, nicely
                  illustrates the discrepancy between the creativity
                  and intuition required in mathematics and the
                  limitations of state of the art theorem provers.},
  Address =	 {Siena, Italy},
  Author =	 {Christoph Benzm{\"u}ller and Manfred Kerber},
  Booktitle =	 {Proceedings of the IJCAR 2001 Workshop: Future
                  Directions in Automated Reasoning},
  Pages =	 {13-24},
  Title =	 {A Lost Proof},
  Note =	 {Url (preprint):
                  \url{http://christoph-benzmueller.de/papers/W13.pdf}},
  Year =	 2001,
}