English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
  Extraction of Proofs from the Clausal Normal Form Transformation

de Nivelle, H. (2002). Extraction of Proofs from the Clausal Normal Form Transformation. In Computer Science Logic: 16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL (pp. 584-598). Berlin, Germany: Springer.

Item is

Files

show Files

Locators

show

Creators

show
hide
 Creators:
de Nivelle, Hans1, Author           
Bradfield, Julian, Editor
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 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.

Details

show
hide
Language(s): eng - English
 Dates: 2003-08-042002
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 202103
Other: Local-ID: C1256104005ECAFC-9D6F3F8E8C3039C0C1256D090039E7D0-deNivelle2002a
 Degree: -

Event

show
hide
Title: CSL 2002
Place of Event: Edinburgh, UK
Start-/End Date: 2002-09-22

Legal Case

show

Project information

show

Source 1

show
hide
Title: Computer Science Logic : 16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL
Source Genre: Proceedings
 Creator(s):
Affiliations:
Publ. Info: Berlin, Germany : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 584 - 598 Identifier: ISBN: 3-540-44240-5

Source 2

show
hide
Title: Lecture Notes in Computer Science
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 2471 Sequence Number: - Start / End Page: - Identifier: -