International Symposium on Multiple-valued Logic, 1999
Bernhard Beckert, Reiner Hähnle, Felip Manya
In the last years two automated reasoning techniques for clause normal
form arose in which the use of labels are prominently featured: signed
logic and annotated logic programming, which can be embedded into the
first. The underlying basic idea is to generalise the classical notion
of a literal by adorning an atomic formula with a sign or label which in
general consists of a possibly ordered set of truth values. In this
paper we relate signed logic and classical logic more closely than
before by defining two new transformations between them. As a byproduct
we obtain a number of new complexity results and proof procedures for
signed logics.