Practically useful variants of definitional translations to normal form

DOI10.1006/INCO.1999.2861zbMath1003.68149OpenAlexW1975422829MaRDI QIDQ1854384

Thomas Rath, Uwe Egly

Publication date: 14 January 2003

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/inco.1999.2861

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (1)

Towards a notion of unsatisfiable and unrealizable cores for LTL

Uses Software

• TPTP
• KoMeT

Cites Work

• Unnamed Item
• Unnamed Item
• 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
• On the practical value of different definitional translations to normal form
• The TPTP problem library

This page was built for publication: Practically useful variants of definitional translations to normal form