Extraction of proofs from the clausal normal form transformation

DOI10.1007/3-540-45793-3_39MaRDI QIDQ4411849zbMATH OpenFDO

Authors Hans de Nivelle

Publication date 10 July 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2471/24710584.htm

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 404251
• Resolution theorem proving
• Optimizing the clausal normal form transformation
• A structure-preserving clause form translation
• Computing small clause normal forms

Cited in

(9)

• Translating higher-order clauses to first-order clauses
• Translation of resolution proofs into short first-order proofs without choice axioms
• Proofs and reconstructions
• MUS Extraction Using Clausal Proofs
• Extracting Information from Logical Proofs
• scientific article; zbMATH DE number 404251 (Why is no real title available?)
• Concurrent inference through dual transformation
• scientific article; zbMATH DE number 2135666 (Why is no real title available?)
• Scalable fine-grained proofs for formula processing

Describes a project that uses

Uses Software

• SPASS
• Ivy

This page was built for publication: Extraction of proofs from the clausal normal form transformation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4411849)