Pages that link to "Item:Q1098330"
From MaRDI portal
The following pages link to A structure-preserving clause form translation (Q1098330):
Displaying 50 items.
- Translating higher-order clauses to first-order clauses (Q2471742) (← links)
- Translation of resolution proofs into short first-order proofs without choice axioms (Q2486578) (← 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)
- Computing small clause normal forms (Q2751358) (← links)
- Range and set abstraction using SAT (Q2814098) (← links)
- nanoCoP: A Non-clausal Connection Prover (Q2817929) (← links)
- On Stronger Calculi for QBFs (Q2818031) (← links)
- A Generalisation of the Hyperresolution Principle to First Order Gödel Logic (Q2829667) (← links)
- Interpolant learning and reuse in SAT-based model checking (Q2864382) (← links)
- Algorithms for Solving Satisfiability Problems with Qualitative Preferences (Q2900530) (← links)
- Optimization Modulo Theories with Linear Rational Costs (Q2946768) (← links)
- Abstraction-Based Algorithm for 2QBF (Q3007686) (← links)
- A Non-clausal Connection Calculus (Q3010371) (← links)
- Propositional SAT Solving (Q3176367) (← links)
- A Fast Symbolic Transformation Based Algorithm for Reversible Logic Synthesis (Q3186608) (← links)
- (Q3384880) (← links)
- Efficient description logic reasoning in Prolog: The DLog system (Q3393230) (← links)
- PBLib – A Library for Encoding Pseudo-Boolean Constraints into CNF (Q3453205) (← links)
- Recognition of Nested Gates in CNF Formulas (Q3453230) (← links)
- QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving (Q3453239) (← links)
- History and Prospects for First-Order Automated Deduction (Q3454079) (← links)
- Ordered Resolution for Coalition Logic (Q3455769) (← links)
- A Modal-Layered Resolution Calculus for K (Q3455770) (← links)
- Inferring Congruence Equations Using SAT (Q3512500) (← links)
- A Direct Algorithm for Multi-valued Bounded Model Checking (Q3540066) (← links)
- Dynamic Symmetry Breaking by Simulating Zykov Contraction (Q3637171) (← links)
- Tableaux for logics of time and knowledge with interactions relating to synchrony (Q3647215) (← links)
- Combining Description Logics, Description Graphs, and Rules (Q3655191) (← links)
- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme (Q3655207) (← links)
- (Q3711782) (← links)
- A temporal negative normal form which preserves implicants and implicates (Q4443401) (← links)
- Lean induction principles for tableaux (Q4610315) (← links)
- Non-elementary speed-ups in proof length by different variants of classical analytic calculi (Q4610324) (← links)
- A resolution-based proof method for temporal logics of knowledge and belief (Q4632296) (← links)
- On the practical value of different definitional translations to normal form (Q4647537) (← links)
- From Schütte’s Formal Systems to Modern Automated Deduction (Q5013905) (← links)
- The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1 (Q5015602) (← links)
- Modal Logic S5 Satisfiability in Answer Set Programming (Q5019595) (← links)
- (Q5146113) (← links)
- (Q5146127) (← links)
- THE FLUTED FRAGMENT REVISITED (Q5195057) (← links)
- Blocked Clause Elimination for QBF (Q5200018) (← links)
- Semantically guided first-order theorem proving using hyper-linking (Q5210771) (← links)
- KoMeT (Q5210812) (← links)
- Some pitfalls of LK-to-LJ translations and how to avoid them (Q5234695) (← links)
- Logic programming with satisfiability (Q5437652) (← links)
- Automated Model Building: From Finite to Infinite Models (Q5505496) (← links)
- Transfer Function Synthesis without Quantifier Elimination (Q5892491) (← links)
