@techreport{R-92-02,
PSURL = {/publications/cgi-bin/tr-fetch.pl?r-92-02+ps},
ABSTRACTURL = {/publications/cgi-bin/tr-fetch.pl?r-92-02+abstr},
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.
},
TITLE = {A Constraint-Based Approach to Proof Procedures for Multi-Valued Logics},
AUTHOR = {Patrick Doherty},
EMAIL = {patdo@ida.liu.se},
YEAR = {1992},
NUMBER = {R-92-02},
INSTITUTION = ida,
ADDRESS = idaaddr,
IDANR = {LiTH-IDA-R-92-02},
NOTE = {Also published in 1st World Conference on the Fundamentals of Artificial Intelligence, Paris, France, 1-5 July 1991}