|
This article is cited in 1 scientific paper (total in 1 paper)
Infinite-valued first-order Łukasiewicz logic: hypersequent calculi without structural rules and proof search for sentences in the prenex form
A. S. Gerasimov
Abstract:
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.
Key words:
fuzzy logic, infinite-valued first-order Łukasiewicz logic, rational first-order Pavelka logic, hypersequent calculus, proof search algorithm.
Received: 21.03.2016
Citation:
A. S. Gerasimov, “Infinite-valued first-order Łukasiewicz logic: hypersequent calculi without structural rules and proof search for sentences in the prenex form”, Mat. Tr., 20:2 (2017), 3–34; Siberian Adv. Math., 28:2 (2018), 79–100
Linking options:
https://www.mathnet.ru/eng/mt321 https://www.mathnet.ru/eng/mt/v20/i2/p3
|
Statistics & downloads: |
Abstract page: | 279 | Full-text PDF : | 110 | References: | 41 | First page: | 7 |
|