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.
On T Logic Programming
A. Dovier;A. Formisano;A. Policriti
1997-01-01
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
