Abstract
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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
B. Beckert, R. Hähnle, P. Oel, and M. Sulzmann. The tableau-based theorem prover 3 T A P, version 4.0. In M. McRobbie and J. Slaney, editors, Proc., 13th International Conference on Automated Deduction (CADE), New Brunswick, NJ, USA, LNCS 1104. Springer, 1996.
R. Hähnle. Many-valued logic and mixed integer programming. Annals of Mathematics and Artificial Intelligence, 12(3,4):231–264, Dec. 1994.
R. Hasegawa. Model generation theorem provers and their applications. In L. Sterling, editor, Proceedings of the 12th International Conference on Logic Programming, pages 7–8, Cambridge, MA, USA, June13-18 1995. MIT Press.
M. Kerber and M. Kohlhase. A mechanization of strong Kleene logic for partial functions. SEKI-Report SR-93-20 (SFB), Universität des Saarlandes, Saarbrücken, 1993.
K. Konrad and D. A. Wolfram. Finite model generation for many-valued higherorder logics. Forthcoming, 1999.
Programming Systems Lab Saarbrücken, 1998. Oz Webpage: http://www.ps.uni-sb.de/oz/.
J. Slaney. FINDER (Finite Domain Enumerator): Notes and guide. Technical Report TR-ARP-1/92, Australian National University Automated Reasoning Project, Canberra, 1992.
C. Suttner and G. Sutcliffe. The TPTP problem library (TPTP v2.2.0). Technical Report 97-04, Department of Computer Science, James Cook University, Townsville, Australia, 1998.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Konrad, K., Wolfram, D.A. (1999). System Description: Kimba, A Model Generator for Many-Valued First-Order Logics. In: Automated Deduction — CADE-16. CADE 1999. Lecture Notes in Computer Science(), vol 1632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48660-7_24
Download citation
DOI: https://doi.org/10.1007/3-540-48660-7_24
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66222-8
Online ISBN: 978-3-540-48660-2
eBook Packages: Springer Book Archive