# Questions tagged [resolution]

The tag has no usage guidance.

12 questions
Filter by
Sorted by
Tagged with
2k views

### Is propositional resolution a complete proof system?

This question is about propositional logic and all occurrences of "resolution" should be read as "propositional resolution". This question is something extremely basic but it has been bothering me ...
129 views

### Direct Proof that the Pigeonhole Principle is Hard for Regular Resolution

It is well known that the pigeonhole principle $PHP_n^{n+1}$ is hard for general resolution. The original proof due to Haken is elegant. One first defines a complexity measure for derived clauses, in ...
88 views

### Axioms of Minimum Size Resolution Refutations

Let $\phi$ be an unsatisfiable CNF formula and let $\Pi$ be a resolution refutation of $\phi$ of minimum size. Let $\psi$ be the subformula of $\phi$ containing the clauses that actually appear as ...
196 views

### Resolution vs Nondeterministic Search Problems

It is well known that each resolution refutation $\Pi$ for an unsatisfiable CNF formula $F = C_1\wedge C_2 \wedge ... \wedge C_m$ over variables $X$ can be translated in polynomial time (in the size ...
222 views

### Mechanization of Mathematics

Its been a while since I took my theory course, but I recall that Hilberts Decision problem was shown to be false. By the completeness theorem of first-order logic, a statement is universally valid ...
186 views

### About Closure under Resolution

The question looks very simple, that is why I posted it first on MathSE, unsuccesfully - no answer for 12 days. I tried to find a short and elegant answer to the question, but I haven't succeed yet. ...
151 views

### resolution based theorem prover for temporal logic

I am looking at implementing a a resolution-based theorem prover for propositional linear temporal logic (PLTL) (as opposed to a model checker). The ones out there (by Fisher et. al. and others) are ...
55 views

### Substitution in Resolution Proofs

Let $F = C_1 \wedge C_2\; \wedge ... \wedge\; C_m$ be a unsatisfiable $k$-CNF on variables $x_1,...,x_n$, where $k$ is constant. Let $x_j\rightarrow x_j^1\wedge x_j^2$ be a substitution that replaces ...
179 views

### Most general form of SAT which is in P

2-SAT is in P. Additionally, a (CNF) SAT-problem is trivially poly-time solvable if no two expressions can be resolved (via Robinson resolution, ie for every pair of disjunctive clauses, they either ...
113 views

### Implied Clause and Resolvent

(I posted this question on MathSE first, no answer, that is the reason why I come here.) Let $F$ be a 3-CNF formula on $n$ variables. A clause $c$ is implied by the formula if $F$ and $F \wedge c$ ...