scientific article; zbMATH DE number 1303351

zbMATH Open0924.03023MaRDI QIDQ4249904FDOQ4249904

Authors: Andreas Nonnengart, Georg Rock, Christoph Weidenbach 

Publication date: 7 November 1999

Title of this publication is not available (Why is that?)

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

zbMATH Keywords

clause normal form transformationrefined Skolemizationrenaming of formulae

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

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
• Computing Tiny Clause Normal Forms
• Binary resolution over complete residuated Stone lattices
• 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
• A \textit{DPLL} procedure with dichotomous branching for propositional product logic
• Hyperresolution for Gödel logic with truth constants
• An optimality result for clause form translation

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)