A structure-preserving clause form translation
From MaRDI portal
Publication:1098330
DOI10.1016/S0747-7171(86)80028-1zbMath0636.68119WikidataQ29031727 ScholiaQ29031727MaRDI QIDQ1098330
Steven Greenbaum, David Alan Plaisted
Publication date: 1986
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Related Items
Extracting unsatisfiable cores for LTL via temporal resolution, Quantified maximum satisfiability, Towards resolution-based reasoning for connected logics, Problem solving by searching for models with a theorem prover, A neural implementation of multi-adjoint logic programming, Binary resolution over complete residuated Stone lattices, Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures, Algorithms for Solving Satisfiability Problems with Qualitative Preferences, Representing ontologies using description logics, description graphs, and rules, PBLib – A Library for Encoding Pseudo-Boolean Constraints into CNF, Recognition of Nested Gates in CNF Formulas, QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving, Propositional SAT Solving, History and Prospects for First-Order Automated Deduction, Ordered Resolution for Coalition Logic, A Modal-Layered Resolution Calculus for K, KBO orientability, Embedding complex decision procedures inside an interactive theorem prover., First-order temporal verification in practice, KoMeT, A Fast Symbolic Transformation Based Algorithm for Reversible Logic Synthesis, Answer set programming based on propositional satisfiability, The SAT-based approach to separation logic, Simulating circuit-level simplifications on CNF, Solving satisfiability problems with preferences, Craig interpolation with clausal first-order tableaux, Minimal sets on propositional formulae. Problems and reductions, An answer to an open problem of Urquhart, Optimization Modulo Theories with Linear Rational Costs, OuterCount: a first-level solution-counter for quantified Boolean formulas, True crafted formula families for benchmarking quantified satisfiability solvers, Hyperresolution for guarded formulae, Inferring Congruence Equations Using SAT, A satisfiability procedure for quantified Boolean formulae, Towards a notion of unsatisfiable and unrealizable cores for LTL, Lean induction principles for tableaux, Non-elementary speed-ups in proof length by different variants of classical analytic calculi, Unnamed Item, Abstract interpretation of microcontroller code: intervals meet congruences, Algorithms for computing minimal equivalent subformulas, Deciding expressive description logics in the framework of resolution, A Direct Algorithm for Multi-valued Bounded Model Checking, A resolution-based decision procedure for \({\mathcal{SHOIQ}}\)., A resolution-based proof method for temporal logics of knowledge and belief, Reasoning in description logics by a reduction to disjunctive datalog, Abstraction-Based Algorithm for 2QBF, A Non-clausal Connection Calculus, Enhancing unsatisfiable cores for LTL with information on temporal relevance, Complexity of resolution proofs and function introduction, On the practical value of different definitional translations to normal form, An interleaved depth-first search method for the linear optimization problem with disjunctive constraints, An optimality result for clause form translation, SAT solver management strategies in IC3: an experimental approach, Combining enumeration and deductive techniques in order to increase the class of constructible infinite models, A new 3-CNF transformation by parallel-serial graphs, Using temporal logics of knowledge for specification and verification -- a case study, On deciding subsumption problems, Logic programming with satisfiability, THE FLUTED FRAGMENT REVISITED, Machine learning guidance for connection tableaux, Blocked Clause Elimination for QBF, Transfer Function Synthesis without Quantifier Elimination, The resolution of Keller's conjecture, Semantically guided first-order theorem proving using hyper-linking, A temporal negative normal form which preserves implicants and implicates, Range and Set Abstraction using SAT, Combining induction and saturation-based theorem proving, \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments, Definability for model counting, nanoCoP: A Non-clausal Connection Prover, On Stronger Calculi for QBFs, A solver for QBFs in negation normal form, Dynamic Symmetry Breaking by Simulating Zykov Contraction, Efficient description logic reasoning in Prolog: The DLog system, A Generalisation of the Hyperresolution Principle to First Order Gödel Logic, Normal Form Nested Programs, Tableaux for logics of time and knowledge with interactions relating to synchrony, Some pitfalls of LK-to-LJ translations and how to avoid them, Combining Description Logics, Description Graphs, and Rules, Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme, Unnamed Item, Unnamed Item, Constructing infinite models represented by tree automata, Hyperresolution for Gödel logic with truth constants, Automated Model Building: From Finite to Infinite Models, An interpolating theorem prover, Practically useful variants of definitional translations to normal form, From Schütte’s Formal Systems to Modern Automated Deduction, The resolution of Keller's conjecture, Interpolant Learning and Reuse in SAT-Based Model Checking, The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1, Local reductions for the modal cube, Modal Logic S5 Satisfiability in Answer Set Programming, HermiT: an OWL 2 reasoner, Clausal resolution in a logic of rational agency, Unrestricted vs restricted cut in a tableau method for Boolean circuits, Solving QBF with counterexample guided refinement, SAT-based planning in complex domains: Concurrency, constraints and nondeterminism, Davis and Putnam meet Henkin: solving DQBF with resolution
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Completely non-clausal theorem proving
- Splitting and reduction heuristics in automatic theorem proving
- On the SUP-INF Method for Proving Presburger Formulas
- Fast Decision Procedures Based on Congruence Closure
- Simplification by Cooperating Decision Procedures
- The Concept of Demodulation in Theorem Proving
