Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
 
 
DownloadE-Mail
 Lokale TagsFreigabegeschichteDetailsÜbersicht
  Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms

de Nivelle, H. (2005). Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms. Information and Computation, 199, 24-54.

Item is

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-2822-F Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-2823-D
Genre: Zeitschriftenartikel

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
de Nivelle, Hans1, Autor           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: We present a way of transforming a resolution-style proof containing Skolemization into a natural deduction proof without Skolemization. The size of the proof increases only moderately (polynomially). This makes it possible to translate the output of a resolution theorem prover into a purely first-order proof that is moderate in size.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2005-12-212005
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: Expertenbegutachtung
 Identifikatoren: eDoc: 279100
Anderer: Local-ID: C1256104005ECAFC-904AC741B97386B6C1256FC10056F74F-deNivelle2005a
 Art des Abschluß: -

Veranstaltung

einblenden:

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Information and Computation
Genre der Quelle: Zeitschrift
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: 199 Artikelnummer: - Start- / Endseite: 24 - 54 Identifikator: -