An optimality result for clause form translation

DOI10.1016/0747-7171(92)90009-SzbMath0772.68079OpenAlexW1996010294MaRDI QIDQ1201346

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

resolution methodchallenge problemclause form translatorsrenamings

Mathematics Subject Classification ID

Related Items

Binary resolution over complete residuated Stone lattices ⋮ Recognition of Nested Gates in CNF Formulas ⋮ Verifying the conversion into CNF in dafny ⋮ Simulating circuit-level simplifications on CNF ⋮ Towards a notion of unsatisfiable and unrealizable cores for LTL ⋮ Parallel rewriting of attributed graphs ⋮ SPASS & FLOTTER version 0.42 ⋮ An interleaved depth-first search method for the linear optimization problem with disjunctive constraints ⋮ Extended resolution simulates binary decision diagrams ⋮ Combining enumeration and deductive techniques in order to increase the class of constructible infinite models ⋮ Translation of resolution proofs into short first-order proofs without choice axioms ⋮ An empirical analysis of modal theorem provers ⋮ \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments ⋮ A solver for QBFs in negation normal form ⋮ A Generalisation of the Hyperresolution Principle to First Order Gödel Logic ⋮ Hyperresolution for Gödel logic with truth constants ⋮ Local reductions for the modal cube

Uses Software

• FLOTTER

Cites Work

• Unnamed Item
• Unnamed Item
• A structure-preserving clause form translation
• Seventy-five problems for testing automatic theorem provers

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