System Description: Kimba, A Model Generator for Many-Valued First-Order Logics

Kimba is the first model generation program which implements a semi-decision procedure for nite satisability of rst-order logics with nitely many truth values. The procedure enumerates the nite models of its input and can be used to compute efficiently domain minimal models whose positive part is minimal in size. Kimba has been implemented in the constraint logic programming language Oz [6] and is based on a tableaux calculus that translates deduction problems into Constraint Satisfaction Problems (CSPs). The constraint propagators needed to solve these problems are realized as concurrent procedures that can make use of Oz’s built-in capabilities for solving CSPs.We describe the current prototype focusing on the method for generating and solving CSPs.