Doherty, P. (1992). A Constraint-Based Approach to Proof Procedures for Multi-Valued Logics. Technical Report LiTH-IDA-R-92-02, Department of Computer and Information Science, Linköping University, Sweden. Also published in 1st World Conference on the Fundamentals of Artificial Intelligence, Paris, France, 1-5 July 1991. (bibtex),
Abstract: In this article, we present a tableau-based theorem-prover for KL*, a three-valued logic, based on Kleene's strong definitions (KL). KL* is derived from KL by extending it with an additional weak negation connective denoting absence of truth. The resulting logic appears to be quite useful in the natural language area, but has had little application in artificial intelligence until recently. Although we are aware of a number of axiomatizations for KL*, the technique described in this article, which is based on generalizing the notion of a signed formula with a single sign to one with a set of signs ordered in a constraint lattice has, to our knowledge, not yet been used in proof techniques for KL*. The use of a constraint lattice on truth-values emphasizes the reading of multiple-truth values as constraints on sentences rather than denotations. Once this view is taken, any set of elements with an appropriate constraint ordering may be incorporated into the technique, a very useful notion in the context of knowledge representation in AI.
CS Dept TR Overview