|Home||Online Resources||Table of Contents|
Journal of Logic and Computation, Volume 8, Issue 4: August 1998.
Simplification of many-valued logic formulas using anti-links
B Beckert, R Hähnle and G Escalada-Imaz1
Universität Karlsruhe, Institut für Logik, Komplexität und Deduktionssysteme, D-76128 Karlsruhe, Germany. E-mail: beckert,firstname.lastname@example.org, 1Institut d'Investigació en Intel.ligeència Artificial, Campus Universitat Autònoma de Barcelona, E-08193 Bellaterra, Barcelona, Spain. E-mail: email@example.com
The theoretical foundations of the many-valued generalization of a technique for simplifying large non-clausal formulas in propositional logic, called removal of anti-links are presented. 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. An anti-link operation on a generic language is defined for expressing many-valued logic formulas called signed NNF and its shown that all interesting properties of a two-valued anti-links generalize to the many-valued setting, although in a non-trivial way.
Key words: Many-valued logic, subsumption, prime implicants/implicates.