Theorem Proving and Logic Programming with Constraints (Dagstuhl Seminar 9143)
Hubert Comon, Harald Ganzinger, Claude Kirchner, Kirchner, Hélène, Jean-Louis Lassez, Gert Smolka · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 1992
We present the constraint system FT, which we feel is an intriguing alternative to Herbrand both theoretically and practically.As does Herbrand, FT provides a universal data structure based on trees.However, the trees of FT (called feature trees) are more general than the trees of Herbrand (called constructor trees), and the constraints of FT are ner grained and of different expressivity.The basic notion of FT are functional attributes called features, which provide for record-like descriptions of data avoiding the overspeci cation intrinsic in Herbrand s constructor based descriptions.The feature tree structure xes an algebraic semantics for FT.We will also establish a logical semantics, which is given by three recursive axiom schemes xing the rst-order theory FT.FT is a constraint system for logic programming, providing a test for unsatis ability, and a test for entailment between constraints, which is needed for advanced control mechanisms.The two major technical contributions of this paper are (1) an incremental entailment simpli cation system that is proved to be sound and complete, and (2) a proof showing that FT satis es the so-called independence of negative constraints.