Pages that link to "Item:Q1201346"
From MaRDI portal
The following pages link to An optimality result for clause form translation (Q1201346):
Displaying 21 items.
- Simulating circuit-level simplifications on CNF (Q352967) (← links)
- An optimal construction of Hanf sentences (Q420856) (← links)
- Towards a notion of unsatisfiable and unrealizable cores for LTL (Q433349) (← links)
- Binary resolution over complete residuated Stone lattices (Q835103) (← links)
- A solver for QBFs in negation normal form (Q1020501) (← links)
- A structure-preserving clause form translation (Q1098330) (← links)
- Using tactics to reformulate formulae for resolution theorem proving (Q1380410) (← links)
- An interleaved depth-first search method for the linear optimization problem with disjunctive constraints (Q1753130) (← links)
- Practically useful variants of definitional translations to normal form (Q1854384) (← links)
- Local reductions for the modal cube (Q2104538) (← links)
- Verifying the conversion into CNF in dafny (Q2148786) (← links)
- Parallel rewriting of attributed graphs (Q2215963) (← links)
- \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments (Q2303247) (← links)
- Hyperresolution for Gödel logic with truth constants (Q2328910) (← links)
- Extended resolution simulates binary decision diagrams (Q2478427) (← links)
- Translation of resolution proofs into short first-order proofs without choice axioms (Q2486578) (← links)
- A Generalisation of the Hyperresolution Principle to First Order Gödel Logic (Q2829667) (← links)
- Recognition of Nested Gates in CNF Formulas (Q3453230) (← links)
- An empirical analysis of modal theorem provers (Q4443417) (← links)
- SPASS & FLOTTER version 0.42 (Q4647508) (← links)
- Combining enumeration and deductive techniques in order to increase the class of constructible infinite models (Q5927982) (← links)
