Geodesic
Infinite-valued first-order {\L}ukasiewicz logic: hypersequent calculi without structural rules and proof search for sentences in the prenex form
Matematičeskie trudy, Tome 20 (2017) no. 2, pp. 3-34.

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

The rational first-order Pavelka logic is an expansion of the infinite-valued first-order Łukasiewicz logic Ł$\forall$ by truth constants. For this logic, we introduce a cumulative hypersequent calculus G$^1$Ł$\forall$ and a noncumulative hypersequent calculus G$^2$Ł$\forall$ without structural inference rules. We compare these calculi with the Baaz–Metcalfe hypersequent calculus GŁ$\forall$ with structural rules. In particular, we show that every GŁ$\forall$-provable sentence is G$^1$Ł$\forall$-provable and a Ł$\forall$-sentence in the prenex form is GŁ$\forall$-provable if and only if it is G$^2$Ł$\forall$-provable. For a tableau version of the calculus G$^2$Ł$\forall$, we describe a family of proof search algorithms that allow us to construct a proof of each G$^2$Ł$\forall$-provable sentence in the prenex form. 
@article{MT_2017_20_2_a0,
     author = {A. S. Gerasimov},
     title = {Infinite-valued first-order {{\L}ukasiewicz} logic: hypersequent calculi without structural rules and proof search for sentences in the prenex form},
     journal = {Matemati\v{c}eskie trudy},
     pages = {3--34},
     publisher = {mathdoc},
     volume = {20},
     number = {2},
     year = {2017},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MT_2017_20_2_a0/}
}
TY  - JOUR
AU  - A. S. Gerasimov
TI  - Infinite-valued first-order {\L}ukasiewicz logic: hypersequent calculi without structural rules and proof search for sentences in the prenex form
JO  - Matematičeskie trudy
PY  - 2017
SP  - 3
EP  - 34
VL  - 20
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MT_2017_20_2_a0/
LA  - ru
ID  - MT_2017_20_2_a0
ER  - 
%0 Journal Article
%A A. S. Gerasimov
%T Infinite-valued first-order {\L}ukasiewicz logic: hypersequent calculi without structural rules and proof search for sentences in the prenex form
%J Matematičeskie trudy
%D 2017
%P 3-34
%V 20
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MT_2017_20_2_a0/
%G ru
%F MT_2017_20_2_a0
A. S. Gerasimov. Infinite-valued first-order {\L}ukasiewicz logic: hypersequent calculi without structural rules and proof search for sentences in the prenex form. Matematičeskie trudy, Tome 20 (2017) no. 2, pp. 3-34. http://geodesic.mathdoc.fr/item/MT_2017_20_2_a0/

[1] Gerasimov A. S., “Predikatnaya logika na osnove sekventsialnogo ischisleniya, prednaznachennaya dlya modelirovaniya nepreryvnykh shkal”, Desyataya natsionalnaya konferentsiya po iskusstvennomu intellektu KII-06, Trudy konferentsii, v. 1, Fizmatlit, M., 2006, 339–347

[2] Gerasimov A. S., Razrabotka i realizatsiya algoritma poiska vyvoda v rasshirenii beskonechnoznachnoi predikatnoi logiki Lukasevicha, Dis. ...kand. fiz.-mat. nauk, S.-Peterburg. gos. un-t, SPb., 2007

[3] Gerasimov A. S., “Semanticheskie tablitsy s metaperemennymi dlya logiki nechetkikh neravenstv”, Algebra i logika, 55:2 (2016), 156–191 | Zbl

[4] Kosovskii N. K., “Urovnevye logiki”, Zap. nauch. seminarov POMI, 220, 1995, 72–82 | Zbl

[5] Maslov S. Yu., Teoriya deduktivnykh sistem i ee primeneniya, Radio i svyaz, M., 1986

[6] Mints G. E., “Skolemovskii metod v intuitsionistskikh ischisleniyakh”, Tr. MIAN SSSR, 121, 1972, 67–99 | Zbl

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

[8] Berend D., Tassa T., “Improved bounds on Bell numbers and on moments of sums of random variables”, Probab. Math. Statist., 30:2 (2010), 185–205 | MR | Zbl

[9] Bongini M., Ciabattoni A., Montagna F., “Proof search and co-NP completeness for many-valued logics”, Fuzzy Sets and Systems, 292 (2016), 130–149 | DOI | MR

[10] Ciabattoni A., Fermüller C. G., Metcalfe G., “Uniform rules and dialogue games for fuzzy logics”, Logic for Programming, Artificial Intelligence, and Reasoning, Lecture Notes in Comput. Sci., 3452, Springer-Verlag, Berlin, 2005, 496–510 | DOI | MR | Zbl

[11] Cintula P., Hájek P., Noguera C. (eds.), Handbook of Mathematical Fuzzy Logic, College Publications, London, 2011 | MR

[12] Fitting M., First-Order Logic and Automated Theorem Proving, 2nd ed., Springer-Verlag, New York, NY, 1996 | MR | Zbl

[13] Gentzen G., “Untersuchungen über das logische Schliessen”, Math. Z., 39 (1935), 176–210 ; 405–431 (German); Gentsen G., “Issledovaniya logicheskikh vyvodov”, Matematicheskaya teoriya logicheskogo vyvoda, Sb. per., eds. A. V. Idelson, G. E. Mints, Nauka, M., 1967, 9–74 | DOI | MR | MR

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

[15] Hájek P., Metamathematics of Fuzzy Logic, Kluwer Academic Publishers, Dordrecht, 1998 | MR

[16] Kaye R., “A Gray code for set partitions”, Inf. Process. Lett., 5:6 (1976), 171–173 | DOI | MR | Zbl

[17] Kleene S. C., Mathematical Logic, Dover Publications, Mineola, NY, 2002 ; Klini S. K., Matematicheskaya logika, LKI, M., 2008 | MR | Zbl | MR

[18] Metcalfe G., Olivetti N., Gabbay D. M., Proof Theory for Fuzzy Logics, Springer, Dordrecht, 2009 | MR | Zbl

[19] Orłowska E., Golińska-Pilarek J., Dual Tableaux: Foundations, Methodology, Case Studies, Springer, Dordrecht, 2011 | MR

[20] Ragaz M. E., Arithmetische Klassifikation von Formelmengen der Unendlichwertigen Logik, PhD Thesis, ETH Zürich, Zürich, 1981

[21] Troelstra A. S., Schwichtenberg H., Basic Proof Theory, 2nd ed., Cambridge Univ. Press, Cambridge, 2000 | MR | Zbl