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