Kimba is the first model generation program which implements a semi-decision procedure for finite satisfiability of first-order logics with finitely many truth values. The procedure enumerates the finite 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.
展开▼
