zbMATH — the first resource for mathematics

The complexity of resolution refinements. (English) Zbl 1160.03005
Much of the research about the satisfiability problem has centered around the method of resolution [J. A. Robinson, “A machine-oriented logic based on the resolution principle”, J. Assoc. Comput. Mach. 12, 23–41 (1965; Zbl 0139.12303)]. This method can be applied to both propositional as well as higher-order theorem proving. Resolution algoritms take as input a formula \(F\) and output a resolution refutation of \(F\) if and only if \(F\) is unsatisfiable. Several variants and refinements of resolution have been investigated in order to determine which particular variant is most efficient for generating resolution refutations. In this paper, the author studies the most popular refinements of resolution and provides a characterization of the relative complexity of these approaches.

03B35 Mechanization of proofs and logical operations
Full Text: DOI Euclid
[1] Studies in constructive mathematics and mathematical logic, part II pp 115– (1968)
[2] DOI: 10.2178/bsl/1203350879 · Zbl 1133.03037
[3] Proceedings of 37th IEEE Foundations of Computer Science pp 234– (1997)
[4] Communications of the ACM 7 pp 201– (1960)
[5] DOI: 10.1145/368273.368557 · Zbl 0217.54002
[6] Conference record of fifth annual ACM Symposium on Theory of Computing pp 29– (1973)
[7] 27th International Colloquium on Automata, Languages and Programming pp 926– (2000)
[8] Proceedings of 40th FOCS pp 422– (1999)
[9] DOI: 10.1137/S0097539799352474 · Zbl 0976.03062
[10] Proceedings of the 34th Annual ACM Symposium on Theory of Computing (STOC-02) pp 457– (2002)
[11] Proceedings of the thirty-first annual ACM Symposium on Theory of Computing pp 517– (1999)
[12] Proceedings of the 34th Annual ACM Symposium on Theory of Computing (STOC-02) pp 448– (2002)
[13] Mathematical Systems Theory 10 pp 239– (1977)
[14] Acta Informatica 22 pp 253– (1985)
[15] 18th Annual Symposium on Foundations of Computer Science pp 254– (1977)
[16] DOI: 10.1016/0004-3702(71)90012-9 · Zbl 0234.68037
[17] DOI: 10.1016/0304-3975(85)90144-6 · Zbl 0586.03010
[18] DOI: 10.1007/BF01531027 · Zbl 0865.03010
[19] DOI: 10.1137/0222044 · Zbl 0781.68099
[20] DOI: 10.1016/0304-3975(92)90216-3 · Zbl 0745.68093
[21] DOI: 10.1145/321250.321253 · Zbl 0139.12303
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.