By Agostino Dovier,
Università di Pisa (consorzio Pisa-Genova-Udine)
March 1996
Abstract
Computable Set Theory investigates the satisfiability problem for fragments of set theory; the CLP scheme allows to automatically obtain logic programming languages dealing with constraints, namely first order fomulae of a given theory, provided a satisfiability test for them exists. The major theme of this thesis is the integration of these two paradigms.
In the first part of the thesis a parametric axiomatization of the theories of lists, multi sets, compact lists, and sets, both in the pure and in the hybrid case (i.e. when also uninterpreted terms are kept into account) is presented, together with the unification algorithms for all of them.
In the second part it is shown how to incorporate such theories in the CLP scheme, by providing algorithms for solving the satisfiability problem via reduction to a normal form. In particular, the set case is analyzed in detail. CLP with sets is then extended with intensional set formers generating the language {log}. Intensional sets are handled using negation: both the negation-as-failure and the constructive negation approach are exploited, showing the different classes of intensional set formers that can be accepted. Examples of the high declarative style of Logic Programming with Sets are given.