PT(CP)-resolution
Fei Liu · 2005
This paper presents the framework of PT(CP)-resolution which is the unification of PT-resolution and conditional proof. PT-resolution is resolution with partial intersection and truncation. The paper analyses the necessity, feasibility and also limitations of this unification and formulates PT(CP)-resolution. PT(CP)-resolution is regarded as an improved version of PT-resolution. It resumes its derivation when the derivation is terminated before the query is answered.