Application of Resolution Games to Resolution Decision Procedures

摘要

The authors apply resolution games to orderings that are used in resolutiondecisions procedures. The authors can prove that the < (sub v) ordering is complete for the class E(sub + 1) without saturation. They define a larger class than the E(sub +)-class, called the T(sub +)-class and show that it can be decided by a generalization of the <(sub v)-ordering, called the <(sub T)-ordering. (Copyright (c) 1994 by Faculty of Technical Mathematics and Informatics, Delft, The Netherlands.)