An optimality result for clause form translation
From MaRDI portal
Publication:1201346
DOI10.1016/0747-7171(92)90009-SzbMath0772.68079OpenAlexW1996010294MaRDI QIDQ1201346
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
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
Cites Work
This page was built for publication: An optimality result for clause form translation
