scientific article; zbMATH DE number 1303351

MaRDI QIDQ4249904zbMATH OpenFDO

Authors Andreas Nonnengart, Georg Rock, Christoph Weidenbach

Publication date 7 November 1999

zbMATH Keywords

clause normal form transformationrefined Skolemizationrenaming of formulae

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Computing small clause normal forms
• Computing Tiny Clause Normal Forms
• Minimizing the number of clauses by renaming
• An optimality result for clause form translation

Cited in

(11)

• Computing Tiny Clause Normal Forms
• Efficiently checking propositional refutations in HOL theorem provers
• An optimality result for clause form translation
• Binary resolution over complete residuated Stone lattices
• Computing small clause normal forms
• Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
• Hyperresolution for Gödel logic with truth constants
• A solver for QBFs in negation normal form
• Effective normalization techniques for HOL
• A Generalisation of the Hyperresolution Principle to First Order Gödel Logic
• A \textit{DPLL} procedure with dichotomous branching for propositional product logic

Describes a project that uses

Uses Software

• TPTP

This page was built for publication:

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