A structure-preserving clause form translation
From MaRDI portal
Publication:1098330
DOI10.1016/S0747-7171(86)80028-1zbMath0636.68119DBLPjournals/jsc/PlaistedG86WikidataQ29031727 ScholiaQ29031727MaRDI QIDQ1098330
Steven Greenbaum, David Alan Plaisted
Publication date: 1986
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Related Items (only showing first 100 items - show all)
True crafted formula families for benchmarking quantified satisfiability solvers ⋮ Minimizing the number of clauses by renaming ⋮ Enhancing SMT-based weighted model integration by structure awareness ⋮ 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 ⋮ 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 ⋮ Unnamed Item ⋮ 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
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
This page was built for publication: A structure-preserving clause form translation
