MPI-INF Logo
Publications

Server    halma.mpi-inf.mpg.de

Proceedings Article, Paper


@InProceedings
Beitrag in Tagungsband, Workshop
Author, Editor
Author(s):
de Nivelle, Hansdblp
Editor(s):
Bradfield, Juliandblp
Not MPII Editor(s):
Bradfield, Julian
BibTeX cite key*:
deNivelle2002a
Title, Booktitle
Title*:
Extraction of Proofs from the Clausal Normal Form Transformation
Booktitle*:
Computer Science Logic : 16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL
Event, URLs
Conference URL::
http://www.dcs.ed.ac.uk/csl02/
Downloading URL:
Event Address*:
Edinburgh, UK
Language:
English
Event Date*
(no longer used):
-- September
Organization:
Event Start Date:
22 September 2002
Event End Date:
25 September 2002
Publisher
Name*:
Springer
URL:
http://www.springer-ny.com
Address*:
Berlin, Germany
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Computer Science
Volume:
2471
Number:
Month:
September
Pages:
584-598
Year*:
2002
VG Wort Pages:
ISBN/ISSN:
3-540-44240-5
Sequence Number:
DOI:
Note, Abstract, ©
(LaTeX) Abstract:
We give techniques for extracting proofs from the
Clausal Normal Form transformation. We discuss and solve three
technical problems:
{\bf (1)}. How to handle the introduction of definitions and Skolem functions.
{\bf (2)}. How to generate short (linear size) proofs.
{\bf (3)}. How to handle optimized Skolemization. We reduce it
to standard Skolemization.
Keywords:
verification. theorem proving
Download
Access Level:
Public

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Audience:
Expert
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort



BibTeX Entry:
@INPROCEEDINGS{deNivelle2002a,
AUTHOR = {de Nivelle, Hans},
 EDITOR = {Bradfield, Julian},
 TITLE = {Extraction of Proofs from the Clausal Normal Form Transformation},
 BOOKTITLE = {Computer Science Logic : 16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL},
 PUBLISHER = {Springer},
 YEAR = {2002},
 VOLUME = {2471},
 PAGES = {584--598},
 SERIES = {Lecture Notes in Computer Science},
 ADDRESS = {Edinburgh, UK},
 MONTH = {September},
 ISBN = {3-540-44240-5},
}

Entry last modified by Christine Kiesel, 03/12/2010
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Hans de Nivelle		Created
04/15/2003 12:32:28 PM
Revisions
5.
4.
3.
2.
1.		Editor(s)
Christine Kiesel
Christine Kiesel
Christine Kiesel
Christine Kiesel
Christine Kiesel		Edit Dates
04.08.2003 16:34:00
04.08.2003 16:29:11
28.07.2003 17:00:18
07.07.2003 15:26:02
14.05.2003 17:24:51