A normal form which preserves 1-tautologies and 0-contradictions in a class of residuum-based propositional fuzzy logics

The most normal forms for fuzzy logics are versions of conjunctive and disjunctive classical normal forms. Unfortunately, they do not preserve neither 1-tautologies nor 0-contradictions. This paper introduces a normal form that partially preserves 1-tautologies for any continuous t-norm - i.e. if a formula is a 1-tautology then their normal form is also a 1-tautology but the reciprocal does not always hold. For the class of t-norms without zero divisors it preserves 0-contradictions, i.e. a formula is 0-contradiction if and only if their normal form is also 0-contradiction. The paper shows that this normal form could be used to implement an automatic theorem provers for a class of residuum-based propositional fuzzy logics.