Pages that link to "Item:Q1098330"
From MaRDI portal
The following pages link to A structure-preserving clause form translation (Q1098330):
Displayed 50 items.
- Solving QBF with counterexample guided refinement (Q253964) (← links)
- Extracting unsatisfiable cores for LTL via temporal resolution (Q266863) (← links)
- Quantified maximum satisfiability (Q272016) (← links)
- Towards resolution-based reasoning for connected logics (Q281156) (← links)
- Simulating circuit-level simplifications on CNF (Q352967) (← links)
- Towards a notion of unsatisfiable and unrealizable cores for LTL (Q433349) (← links)
- Algorithms for computing minimal equivalent subformulas (Q460638) (← links)
- Enhancing unsatisfiable cores for LTL with information on temporal relevance (Q507378) (← links)
- SAT solver management strategies in IC3: an experimental approach (Q526434) (← links)
- Solving satisfiability problems with preferences (Q606909) (← links)
- Unrestricted vs restricted cut in a tableau method for Boolean circuits (Q812394) (← links)
- SAT-based planning in complex domains: Concurrency, constraints and nondeterminism (Q814472) (← links)
- Binary resolution over complete residuated Stone lattices (Q835103) (← links)
- Representing ontologies using description logics, description graphs, and rules (Q840831) (← links)
- KBO orientability (Q846165) (← links)
- First-order temporal verification in practice (Q851137) (← links)
- Answer set programming based on propositional satisfiability (Q861709) (← links)
- The SAT-based approach to separation logic (Q862390) (← links)
- Deciding expressive description logics in the framework of resolution (Q924723) (← links)
- A resolution-based decision procedure for \({\mathcal{SHOIQ}}\). (Q928657) (← links)
- A new 3-CNF transformation by parallel-serial graphs (Q976123) (← links)
- A solver for QBFs in negation normal form (Q1020501) (← links)
- Constructing infinite models represented by tree automata (Q1044230) (← links)
- An answer to an open problem of Urquhart (Q1129262) (← links)
- Complexity of resolution proofs and function introduction (Q1194246) (← links)
- An optimality result for clause form translation (Q1201346) (← links)
- Problem solving by searching for models with a theorem prover (Q1337680) (← links)
- Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures (Q1340966) (← links)
- Embedding complex decision procedures inside an interactive theorem prover. (Q1353946) (← links)
- Hyperresolution for guarded formulae (Q1404983) (← links)
- A satisfiability procedure for quantified Boolean formulae (Q1408385) (← links)
- Clausal resolution in a logic of rational agency (Q1606116) (← links)
- Minimal sets on propositional formulae. Problems and reductions (Q1677431) (← links)
- An interleaved depth-first search method for the linear optimization problem with disjunctive constraints (Q1753130) (← links)
- On deciding subsumption problems (Q1777407) (← links)
- Practically useful variants of definitional translations to normal form (Q1854384) (← links)
- A neural implementation of multi-adjoint logic programming (Q1884271) (← links)
- Machine learning guidance for connection tableaux (Q2031418) (← links)
- Local reductions for the modal cube (Q2104538) (← links)
- Davis and Putnam meet Henkin: solving DQBF with resolution (Q2118283) (← links)
- Combining induction and saturation-based theorem proving (Q2303240) (← links)
- \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments (Q2303247) (← links)
- Definability for model counting (Q2303508) (← links)
- Hyperresolution for Gödel logic with truth constants (Q2328910) (← links)
- HermiT: an OWL 2 reasoner (Q2351420) (← links)
- Abstract interpretation of microcontroller code: intervals meet congruences (Q2442953) (← links)
- Reasoning in description logics by a reduction to disjunctive datalog (Q2462648) (← links)
- Using temporal logics of knowledge for specification and verification -- a case study (Q2494726) (← links)
- An interpolating theorem prover (Q2575736) (← links)
- Craig interpolation with clausal first-order tableaux (Q2666953) (← links)