Independence of Selecting Rule and Ordering Rule in PT-Resolution

摘要

Resolution with Partial Intersection and Truncation (PT-resolution) has been introduced as a new derivation strategy in Logic Programming. A significant advantage of the resolution is that it prevents some derivations from infinite recursion. This paper concentrates on the independence of selecting rule and ordering rule of PT-resolution. It is proven that a PT-derivation is independent from the selecting rule and that a PT-derivation is independent from the ordering rule.