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/