Pages that link to "Item:Q5613969"
From MaRDI portal
The following pages link to A Computing Procedure for Quantification Theory (Q5613969):
Displaying 50 items.
- An efficient algorithm for the 3-satisfiability problem (Q1200758) (← links)
- Graph properties for normal logic programs (Q1208418) (← links)
- On the role of unification in mechanical theorem proving (Q1225469) (← links)
- On the complexity of regular resolution and the Davis-Putnam procedure (Q1249435) (← links)
- Prolog technology for default reasoning: proof theory and compilation techniques (Q1275596) (← links)
- Linear programs for constraint satisfaction problems (Q1278588) (← links)
- How good are branching rules in DPLL? (Q1281405) (← links)
- Length of prime implicants and number of solutions of random CNF formulae (Q1285568) (← links)
- A two-phase algorithm for solving a class of hard satisfiability problems (Q1306378) (← links)
- Simplification in a satisfiability checker for VLSI applications (Q1312163) (← links)
- An exact algorithm for the constraint satisfaction problem: Application to logical inference (Q1313760) (← links)
- Inference flexibility in Horn clause knowledge bases and the simplex method (Q1319393) (← links)
- A kind of logical compilation for knowledge bases (Q1331921) (← links)
- Tractability through symmetries in propositional calculus (Q1332641) (← links)
- Problem solving by searching for models with a theorem prover (Q1337680) (← links)
- On problems with short certificates (Q1338895) (← links)
- Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures (Q1340966) (← links)
- Minimization of a quadratic pseudo-Boolean function (Q1341991) (← links)
- Easy problems are sometimes hard (Q1342226) (← links)
- Ordered model trees: A normal form for disjunctive deductive databases (Q1344891) (← links)
- Embedding complex decision procedures inside an interactive theorem prover. (Q1353946) (← links)
- Davis-Putnam resolution versus unrestricted resolution (Q1353991) (← links)
- An average case analysis of a resolution principle algorithm in mechanical theorem proving. (Q1353997) (← links)
- Branch-and-cut solution of inference problems in propositional logic (Q1356213) (← links)
- Solving propositional satisfiability problems (Q1356218) (← links)
- Disjunctive stable models: Unfounded sets, fixpoint semantics, and computation (Q1363783) (← links)
- A BDD SAT solver for satisfiability testing: An industrial case study (Q1380431) (← links)
- A fast parallel SAT-solver -- efficient workload balancing (Q1380435) (← links)
- Local and global relational consistency (Q1391940) (← links)
- Resolution lower bounds for the weak functional pigeonhole principle. (Q1401365) (← links)
- Approximating minimal unsatisfiable subformulae by means of adaptive core search (Q1408373) (← links)
- How to fake an RSA signature by encoding modular root finding as a SAT problem (Q1408375) (← links)
- Worst-case upper bounds for MAX-2-SAT with an application to MAX-CUT. (Q1408377) (← links)
- Worst-case study of local search for MAX-\(k\)-SAT. (Q1408379) (← links)
- On the structure of some classes of minimal unsatisfiable formulas (Q1408380) (← links)
- Equivalent literal propagation in the DLL procedure (Q1408382) (← links)
- A satisfiability procedure for quantified Boolean formulae (Q1408385) (← links)
- Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. (Q1426130) (← links)
- Relative efficiency of propositional proof systems: Resolution vs. cut-free LK (Q1577476) (← links)
- Complexity-theoretic models of phase transitions in search problems (Q1583531) (← links)
- Alternative foundations for Reiter's default logic (Q1589575) (← links)
- Backtracking tactics in the backtrack method for SAT (Q1596804) (← links)
- Proving unsatisfiability of CNFs locally (Q1610678) (← links)
- An algorithm based on tabu search for satisfiability problem (Q1613279) (← links)
- A note about \(k\)-DNF resolution (Q1641156) (← links)
- P\(_-\)UNSAT approach of attractor calculation for Boolean gene regulatory networks (Q1642530) (← links)
- Relating size and width in variants of Q-resolution (Q1653019) (← links)
- Lower bound on average-case complexity of inversion of Goldreich's function by drunken backtracking algorithms (Q1678752) (← links)
- Efficient, verified checking of propositional proofs (Q1687744) (← links)
- Semantically-guided goal-sensitive reasoning: inference system and completeness (Q1707598) (← links)