Substitutions into propositional tautologies |
| |
| Authors: | Jan Krají?ek |
| |
| Affiliation: | Isaac Newton Institute, Cambridge, CB3 OEH, UK |
| |
| Abstract: | We prove that there is a polynomial time substitution (y1,…,yn):=g(x1,…,xk) with k?n such that whenever the substitution instance A(g(x1,…,xk)) of a 3DNF formula A(y1,…,yn) has a short resolution proof it follows that A(y1,…,yn) is a tautology. The qualification “short” depends on the parameters k and n. |
| |
| Keywords: | Computational complexity Proof complexity Automated theorem proving |
| 本文献已被 ScienceDirect 等数据库收录！ |
|
