@inproceedings{fab9e29eaee14e349ed041e7c7a00203,
title = "Extraction of proofs from the clausal normal form transformation",
abstract = "This paper discusses the problem of how to transform a firstorder formula into clausal normal form, and to simultaneously construct a proof that the clausal normal form is correct. This is relevant for applications of automated theorem proving where people want to be able to use theorem prover without having to trust it.",
author = "\{de Nivelle\}, Hans",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2002.; 16th International Workshop on Computer Science Logic, CSL 2002 and 11th Annual Conference of the European Association for Computer Science Logic, EACSL 2002 ; Conference date: 22-09-2002 Through 25-09-2002",
year = "2002",
doi = "10.1007/3-540-45793-3\_39",
language = "English",
isbn = "3540442405",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "584--598",
editor = "Julian Bradfield",
booktitle = "Computer Science Logic - 16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL 2002, Proceedings",
address = "Germany",
}