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)

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

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)