On T Logic Programming

Abstract

T-resolution parametrically generalizes standard resolution with respect to a first-order theory T (the parameter). The inherent power of its derivation rule, however, makes it difficult to develop efficient unrestricted T -resolution based systems. CLP(X) parametrically extends Horn clause logic program- ming with respect to a domain of computation X . The theory T underlying the domain X is fixed a-priori and can not be modified (extended) by the user. In this paper we present the parametric logic programming language T logic programming (TLP) which extends the CLP-scheme by giving the possibility of acting on the theory T. The scheme is embedded into (linear) T-resolution; however, its syntax ensures that three rules (simple instances of the general T-resolution rule) are sufficient to implement the derivation process.