###
UNIVERSITA` DEGLI STUDI DI PISA

DIPARTIMENTO DI INFORMATICA

Ph.D. Thesis: TD--1/96

##
Computable Set Theory

and

Logic Programming

Agostino Dovier

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.
PDF Version of the complete thesis