Geodesic
Free-variable semantic tableaux for the logic of fuzzy inequalities
Algebra i logika, Tome 55 (2016) no. 2, pp. 156-191.

Voir la notice de l'article provenant de la source Math-Net.Ru

We present a free-variable tableau calculus for the logic of fuzzy inequalities F$\forall$, which is an extension of infinite-valued first-order Lukasiewicz logic Ł$\forall$. The set of all Ł$\forall$-sentences provable in the hypersequent calculus of Baaz and Metcalfe for Ł$\forall$ is embedded into the set of all F$\forall$-sentences provable in the given tableau calculus. We prove NP-completeness of the problem of checking tableau closability and propose an algorithm, which is based on unification, for solving the problem.
Keywords: fuzzy logic, infinite-valued first-order Lukasiewicz logic, automatic proof search, hypersequent calculus, NP-complete problem.
Mots-clés : tableau calculus, tableau closability 
@article{AL_2016_55_2_a1,
     author = {A. S. Gerasimov},
     title = {Free-variable semantic tableaux for the logic of fuzzy inequalities},
     journal = {Algebra i logika},
     pages = {156--191},
     publisher = {mathdoc},
     volume = {55},
     number = {2},
     year = {2016},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/AL_2016_55_2_a1/}
}
TY  - JOUR
AU  - A. S. Gerasimov
TI  - Free-variable semantic tableaux for the logic of fuzzy inequalities
JO  - Algebra i logika
PY  - 2016
SP  - 156
EP  - 191
VL  - 55
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/AL_2016_55_2_a1/
LA  - ru
ID  - AL_2016_55_2_a1
ER  - 
%0 Journal Article
%A A. S. Gerasimov
%T Free-variable semantic tableaux for the logic of fuzzy inequalities
%J Algebra i logika
%D 2016
%P 156-191
%V 55
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/AL_2016_55_2_a1/
%G ru
%F AL_2016_55_2_a1
A. S. Gerasimov. Free-variable semantic tableaux for the logic of fuzzy inequalities. Algebra i logika, Tome 55 (2016) no. 2, pp. 156-191. http://geodesic.mathdoc.fr/item/AL_2016_55_2_a1/

[1] P. Hájek, Metamathematics of fuzzy logic, Trends Log. Stud. Log. Libr., 4, Kluwer Academic Publ., Dordrecht, 1998 | MR | Zbl

[2] P. Cintula, P. Hájek, C. Noguera (eds.), Handbook of mathematical fuzzy logic, v. 1, 2, Stud. Log. (Lond.), 37, 38, Coll. Publ., 2011 | Zbl

[3] M. Baaz, G. Metcalfe, “Herbrand's theorem, Skolemization and proof systems for first-order Lukasiewicz logic”, J. Log. Comput., 20:1 (2010), 35–54 | DOI | MR | Zbl

[4] G. Metcalfe, N. Olivetti, D. Gabbay, Proof theory for fuzzy logics, Appl. Log. Ser., 36, Springer-Verlag, Dordrecht, 2009 | MR | Zbl

[5] A. S. Gerasimov, “Predikatnaya logika na osnove sekventsialnogo ischisleniya, prednaznachennaya dlya modelirovaniya nepreryvnykh shkal”, Desyataya nats. konf. po iskusstv. intellektu KII-06, Tr. konf., Fizmatlit, M., 2006, 339–347

[6] A. S. Gerasimov, Razrabotka i realizatsiya algoritma poiska vyvoda v rasshirenii beskonechnoznachnoi predikatnoi logiki Lukasevicha, Diss. na soisk. uchen. step. kand. fiz.-mat. nauk, S.-Peterburg. gos. un-t, 2007

[7] S. Yu. Maslov, G. E. Mints, “Teoriya poiska vyvoda i obratnyi metod”, Matematicheskaya logika i avtomaticheskoe dokazatelstvo teorem, Nauka, M., 1983, 291–314 | MR

[8] Z. Hóu, A. Tiu, R. Goré, “A labelled sequent calculus for BBI: proof theory and proof search”, Automated reasoning with analytic tableaux and related methods, Proc. 22th int. conf. TABLEAUX 2013 (Nancy, France, September 16–19, 2013), Lecture Notes in Comput. Sci., 8123, eds. D. Galmiche et al., Springer-Verlag, Berlin, 2013, 172–187 | DOI | MR | Zbl

[9] R. M. Smullyan, First-order logic, Dover Publications, New York, 1995 | MR

[10] M. Fitting, First-order logic and automated theorem proving, Grad. Texts Comput. Sci., 2nd ed., Springer-Verlag, New York, NY, 1996 | MR | Zbl

[11] A. Degtyarev, A. Voronkov, “Equality reasoning in sequent-based calculi”, Handbook of automated reasoning, v. I, eds. A. Robinson et al., North-Holland/Elsevier, Amsterdam, 2001, 611–706 | DOI | Zbl

[12] R. Hähnle, P. H. Schmitt, “The liberalized $\delta$-rule in free variable semantic tableaux”, J. Autom. Reasoning, 13:2 (1994), 211–221 | DOI | MR | Zbl

[13] N. K. Kosovskii, A. V. Tishkov, “Polinomialnye algoritmy ustanovleniya sovmestnosti v ratsionalnykh i tselykh chislakh sistem strogikh i nestrogikh lineinykh neravenstv”, Aktualnye problemy sovremennoi matematiki, v. 3, Izd-vo NII MIOO Novosibirskogo gos. un-ta, Novosibirsk, 1997, 95–100

[14] M. S. Paterson, M. N. Wegman, “Linear unification”, J. Comput. Syst. Sci., 16:2 (1978), 158–167 | DOI | MR | Zbl

[15] M. Giese, Proof search without backtracking for free variable tableaux, PhD thesis, Univ. Karlsruhe, 2002

[16] D. E. Knuth, The art of computer programming, Part 1, v. 4A, Combinatorial algorithms, Addison-Wesley, Upper Sadlle River, NJ, 2011 ; D. E. Knut, Iskusstvo programmirovaniya, Ch. 1, v. 4A, Kombinatornye algoritmy, I. D. Vilyams, M., 2013 | MR

[17] S. A. Norgela, “Minus-normalnye sekventsialnye ischisleniya”, Kibernetika, 1977, no. 3, 33–38 | MR | Zbl

[18] S. P. Odintsov, S. O. Speranskii, S. A. Drobyshevich, Vvedenie v neklassicheskie logiki, Ucheb. posobie, RITs NGU, Novosibirsk, 2014