Journal of Logic and Computation
Bernhard Beckert, Reiner Haehnle, Gonzalo Escalada Imaz
We present the theoretical foundations of the many-valued
generalization of a technique for simplifying large non-clausal
formulas in propositional logic, that is called removal of
anti-links. Possible applications include computation of prime
implicates of large non-clausal formulas as required, for example,
in diagnosis. With the anti-link technique, one does not compute
any normal form of a given formula; rather, one removes certain
forms of redundancy from formulas in negation normal form
(NNF). Its main advantage is that no clausal normal form has to be
computed in order to remove redundant parts of a formula. In this
paper, we define an anti-link operation on a generic language for
expressing many-valued logic formulas called signed NNF and we
show that all interesting properties of two-valued anti-links
generalize to the many-valued setting, although in a non-trivial
way.