×

Free-variable semantic tableaux for the logic of fuzzy inequalities. (English. Russian original) Zbl 1386.03025

Algebra Logic 55, No. 2, 103-127 (2016); translation from Algebra Logika 55, No. 2, 156-191 (2016); erratum ibid. 55, No. 3, 256 (2016).
Summary: We present a free-variable tableau calculus for the logic of fuzzy inequalities \(\mathrm{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 Fsentences 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.

MSC:

03B52 Fuzzy logic; logic of vagueness
03F03 Proof theory in general (including proof-theoretic semantics)
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] P. Hájek, Metamathematics of Fuzzy Logic, Trends Log. Stud. Log. Libr., 4, Kluwer, Dordrecht (1998). · Zbl 0937.03030
[2] P. Cintula, P. Hájek, and C. Noguera (eds.), Handbook of Mathematical Fuzzy Logic, Vols. 1, 2, Coll. Publ., London (2011). · Zbl 1284.03177
[3] M. Baaz and G. Metcalfe, “Herbrand’s theorem, Skolemization and proof systems for firstorder Lukasiewicz logic,” J. Log. Comput., 20, No. 1, 35-54 (2010). · Zbl 1188.03014 · doi:10.1093/logcom/exn059
[4] G. Metcalfe, N. Olivetti, and D. Gabbay, Proof Theory for Fuzzy Logics, Appl. Log. Ser., 36, Springer-Verlag, Dordrecht (2009). · Zbl 1168.03002
[5] A. S. Gerasimov, “A sequent calculus-based predicate logic meant for modeling of continuous scales,” in Proc. of the Tenth National Conf. on Artificial Intelligence CAI-06, Obninsk, 2006, pp. 339-347.
[6] A. S. Gerasimov, “Design and implementation of a proof search algorithm for an extension of infinite-valued predicate Lukasiewicz logic,” Ph. D. Thesis, SPbU, St. Petersburg (2007).
[7] S. Yu. Maslov and G. E. Mints, “Theory of proof search and the inverse method,” in Ch. Chang and R. Lee, Symbolic Logic and Mechanical Theorem Proving [Russian translation], Nauka, Moscow (1983), pp. 291-314.
[8] Z. Hóu, A. Tiu, and R. Goré, “A labelled sequent calculus for BBI: Proof theory and proof search,” in Lecture Notes Comput. Sci., 8123, Springer-Verlag, Berlin (2013), pp. 172-187. · Zbl 1401.03098
[9] R. M. Smullyan, First-Order Logic, Dover Publ., New York (1995). · Zbl 0172.28901
[10] M. Fitting, First-Order Logic and Automated Theorem Proving, 2nd ed., Grad. Texts Comput. Sci., Springer-Verlag, New York (1996). · Zbl 0848.68101 · doi:10.1007/978-1-4612-2360-3
[11] A. Degtyarev and A. Voronkov, “Equality reasoning in sequent-based calculi,” in Handbook of Automated Reasoning, A. Robinson et al. (eds.), Vol. 1, North-Holland/Elsevier, Amsterdam (2001), pp. 611-706. · Zbl 1011.03004
[12] R. Hähnle and P. H. Schmitt, “The liberalized <Emphasis Type=”Italic“>δ-rule in free variable semantic tableaux,” J. Autom. Reas., 13, No. 2 (1994), 211-221. · Zbl 0826.03005
[13] N. K. Kosovski and A. V. Tishkov, “Polynomial algorithms for establishing consistency in rational numbers and integers of systems of strict and nonstrict linear inequalities,” in Topical Problems of Modern Mathematics, Vol. 3, NII MIOO NGU, Novosibirsk (1997), pp. 95-100. · Zbl 0921.90117
[14] M. S. Paterson and M. N. Wegman, “Linear unification,” J. Comput. Syst. Sci., 16, No. 2, 158-167 (1978). · Zbl 0371.68013 · doi:10.1016/0022-0000(78)90043-0
[15] M. Giese, “Proof search without backtracking for free variable tableaux,” Ph. D. Thesis, Univ. Karlsruhe (2002).
[16] D. E. Knuth, The Art of Computer Programming, Vol. 4A: Combinatorial Algorithms, Part 1, Addison-Wesley, Upper Sadlle River, NJ (2011) · Zbl 1354.68001
[17] S. A. Norgela, “Minus-normal sequential calculi,” Kibernetika, No. 3, 33-38 (1977). · Zbl 0359.02006
[18] S. P. Odintsov, S. O. Speranski, and S. A. Drobyshevich Introduction to Nonclassical Logics [in Russian], NGU, Novosibirsk (2014).
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.