An optimality result for clause form translation

DOI10.1016/0747-7171(92)90009-SMaRDI QIDQ1201346zbMATH OpenOpenAlexFDO

Authors Thierry Boy de la Tour

Publication date 17 January 1993

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0747-7171(92)90009-s

zbMATH Keywords

challenge problemclause form translatorsrenamingsresolution method

Mathematics Subject Classification ID

Recommendations

• Minimizing the number of clauses by renaming
• A structure-preserving clause form translation
• scientific article; zbMATH DE number 1303351
• Computing Tiny Clause Normal Forms
• Optimizing the clausal normal form transformation

Cites work

• A structure-preserving clause form translation
• scientific article; zbMATH DE number 3870637 (Why is no real title available?)
• scientific article; zbMATH DE number 3420722 (Why is no real title available?)
• Minimizing the number of clauses by renaming
• Seventy-five problems for testing automatic theorem provers

Cited in

(23)

• A solver for QBFs in negation normal form
• A structure-preserving clause form translation
• Using tactics to reformulate formulae for resolution theorem proving
• An interleaved depth-first search method for the linear optimization problem with disjunctive constraints
• Practically useful variants of definitional translations to normal form
• Local reductions for the modal cube
• Verifying the conversion into CNF in dafny
• Parallel rewriting of attributed graphs
• \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
• Hyperresolution for Gödel logic with truth constants
• Extended resolution simulates binary decision diagrams
• Translation of resolution proofs into short first-order proofs without choice axioms
• A Generalisation of the Hyperresolution Principle to First Order Gödel Logic
• Recognition of Nested Gates in CNF Formulas
• Simulating circuit-level simplifications on CNF
• An optimal construction of Hanf sentences
• scientific article; zbMATH DE number 1303351 (Why is no real title available?)
• Towards a notion of unsatisfiable and unrealizable cores for LTL
• An empirical analysis of modal theorem provers
• SPASS \& FLOTTER version 0.42
• Combining enumeration and deductive techniques in order to increase the class of constructible infinite models
• On CNF conversion for SAT and SMT enumeration
• Binary resolution over complete residuated Stone lattices

Describes a project that uses

Uses Software

• FLOTTER

This page was built for publication: An optimality result for clause form translation

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