Minimizing the number of clauses by renaming

DOI10.1007/3-540-52885-7_114MaRDI QIDQ6488560zbMATH OpenFDO

Authors Thierry Boy de la Tour

Publication date 28 April 2023

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Removing redundancy from a clause
• Renaming a set of non-Horn clauses
• scientific article; zbMATH DE number 1090102
• Eliminating Redundant Clauses in SAT Instances
• Preprocessing of propagation redundant clauses
• Preprocessing of propagation redundant clauses
• Simplifying CDCL clause database reduction
• scientific article; zbMATH DE number 4164189
• scientific article; zbMATH DE number 3892614

Cites work

• scientific article; zbMATH DE number 41806 (Why is no real title available?)
• A structure-preserving clause form translation
• Seventy-five problems for testing automatic theorem provers

Cited in

(7)

• Removing redundancy from a clause
• A Mizar mode for HOL
• A structure-preserving clause form translation
• On the practical value of different definitional translations to normal form
• Practically useful variants of definitional translations to normal form
• An optimality result for clause form translation
• Solving strong controllability of temporal problems with uncertainty using SMT

This page was built for publication: Minimizing the number of clauses by renaming

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