Constraint Model Elimination and a PTTP-Implementation

In constraint logic programming, proof procedures for Horn clauses are enhanced with an interface to efficient constraint solvers. In this paper we show how to incorporate constraint processing into a general, non-Horn theorem proving calculus. A framework for a new calculus is introduced which combines model elimination with constraint solving, following the lines of B¨urckert (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.

• Type: Conference
• Year: 1995
• Where: TABLEAUX
• Authors: Peter Baumgartner, Frieder Stolzenburg
• Keywords: Artificial Intelligence, Constraint Logic Programming, Efficient Constraint Solvers, Model Elimination, TABLEAUX 1995