zbMATH — the first resource for mathematics

Resolution games and non-liftable resolution orderings. (English) Zbl 1044.03506
Pacholski, Leszek (ed.) et al., Computer science logic. 8th workshop, CSL ’94, Kazimierz, Poland, September 25-30, 1994. Selected papers. Berlin: Springer-Verlag (ISBN 3-540-60017-5). Lect. Notes Comput. Sci. 933, 279-293 (1995).
Summary: We prove the completeness of the combination of ordered resolution and factoring for a large class of non-liftable orderings, without the need for any additional rules like saturation. This is possible because of a new proof method wich avoids making use of the standard ordered lifting theorem. This proof method is based on resolution games.
For the entire collection see [Zbl 0847.00048].

03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)