On the practical value of different definitional translations to normal form

DOI10.1007/3-540-61511-3_103zbMath1412.68219OpenAlexW1528868468MaRDI QIDQ4647537

Uwe Egly, Thomas Rath

Publication date: 15 January 2019

Published in: Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61511-3_103

zbMATH Keywords

normal formnatural deductiondisjunctive normal formautomated deductiontheorem prover

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Combining enumeration and deductive techniques in order to increase the class of constructible infinite models ⋮ KoMeT ⋮ Practically useful variants of definitional translations to normal form

Uses Software

• TPTP

Cites Work

• On different structure-preserving translations to normal form
• A structure-preserving clause form translation
• A Prolog technology theorem prover: A new exposition and implementation in Prolog
• Controlled integration of the cut rule into connection tableau calculi
• A note on assumptions about Skolem functions
• Theorem Proving via General Matings
• Semantically guided first-order theorem proving using hyper-linking
• The TPTP problem library
• Unnamed Item
• Unnamed Item
• Unnamed Item