@inproceedings{bf1994053e1c43849f652e2193731d7d,
title = "Automated proof construction in type theory using resolution",
abstract = "We provide techniques to integrate resolution logic with equality in type theory. The results may be rendered as follows. - A clausification procedure in type theory, equipped with a correctness proof, all encoded using higher-order primitive recursion. - A novel representation of clauses in minimal logic such that the -representation of resolution proofs is linear in the size of the premisses. - A translation of resolution proofs into lambda terms, yielding a veri fication procedure for those proofs. - The power of resolution theorem provers becomes available in interactive proof construction systems based on type theory.",
author = "Marc Bezem and Dimitri Hendriks and \{De Nivelle\}, Hans",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2000.; 17th International Conference on Automated Deduction, CADE 2000 ; Conference date: 17-06-2000 Through 20-06-2000",
year = "2000",
doi = "10.1007/10721959\_10",
language = "English",
series = "Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)",
publisher = "Springer Verlag",
pages = "148--163",
editor = "David McAllester",
booktitle = "Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings",
address = "Germany",
}