Logic Programming

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 programming 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. Keywords: Theorem Proving, Constraint Logic Programming, Foundations. 1 Introduction The main motivation of this work is to establish a link between automat..