Graded tableaux for Rational Pavelka Logic

In this article, a sound and complete tableau system for Rational Pavelka Logic (RPL) is introduced. Extended formulas are used as the counterpart of the graded formulas. In this calculus, if we want to show that the graded formula (x, r) is tableau provable (in the finite fuzzy theory F, respectively), we develop a tableau for the extended formula [r, x] (for the set of extended formulas {[r,x],[x(1),a(1)],...,[x(n), a(n)]}, respectively). If this tableau closes we claim that (x, r) is tableau provable (in the fuzzy theory F, respectively). We claim also that x is valid at the degree equal to the l.u.b. that allows the closure of the tableaux. Our tableaux are a first step toward efficient procedures of automated deduction in narrow fuzzy logic with truth constants. (c) 2005 Wiley Periodicals, Inc.