Constraint model elimination and a PTTP-implementation

Abstract

In constraint logic programming, proof procedures for Horn clauses are enhanced with an interface to efficient constraint solvers. The question arises whether it is possible to incorporate constraint processing into general, non-Horn theorem proving calculi. In this paper, a positive answer to this question will be given. A framework for a new calculus is introduced which combines model elimination with constraint solving, following the lines of Bürckert (1991). A prototype system has been implemented rapidly by only combining a PROLOG technology implementation of model elimination and PROLOG with constraints. Some example studies, e.g. taxonomic reasoning, show the advantages and some problems with this procedure. Show more