MNiBLoS: a SMT-based solver for continuous t-norm based logics and some of their modal expansions. (English) Zbl 1428.68346
Summary: In the literature, little attention has been paid to the development of solvers for systems of mathematical fuzzy logic, and in particular, there are few works concerned with infinitely-valued logics. In this paper it is presented mNiBLoS (a modal Nice BL-Logics Solver): a modular SMT-based solver complete with respect to a wide family of continuous t-norm based fuzzy modal logics (both with finite and infinite universes), restricting the modal structures to the finite ones. At the propositional level, the solver works with some of the best known infinitely-valued fuzzy logics (including BL, Łukasiewicz, Gödel and product logics), and with all the continuous t-norm based logics that can be finitely expressed in terms of the previous ones; concerning the modal expansion, mNiBLoS imposes no boundary on the cardinality of the modal structures considered. The solver allows to test 1-satisfiability of equations, tautologicity and logical consequence problems. The logical language supported extends the usual one of fuzzy modal logics with rational constants and the Monteiro-Baaz \(\Delta\) operator. The code of mNiBLoS is of free distribution and can be found in the web page of the author.
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
| 03B52 | Fuzzy logic; logic of vagueness |
Keywords:
fuzzy logic; modal logic; automated reasoning; continuous t-norms; SMT; infinite-valued logicReferences:
| [1] | Agliano, P.; Montagna, F., Varieties of BL-algebras. I. General properties, J. Pure Appl. Algebra, 181, 2-3, 105-129 (2003) · Zbl 1034.06009 |
| [2] | Aguzzoli, S.; Gerla, B., On countermodels in Basic Logic, Neural Netw. World, 12, 5, 407-421 (2002) |
| [3] | Aguzzoli, S.; Gerla, B.; Haniková, Z., Complexity issues in basic logic, Soft Comput., 9, 12, 919-934 (2005) · Zbl 1093.03010 |
| [4] | Alsinet, T.; Barroso, D.; Béjar, R.; Bou, F.; Cerami, M.; Esteva, F., On the implementation of a fuzzy dl solver over infinite-valued product logic with smt solvers, Proceedings of the Scalable Uncertainty Management (SUM2013), Lecture Notes in Computer Science, 8078, 325-330 (2013), Springer |
| [5] | Ansótegui, C.; Bofill, M.; Manyà, F.; Villaret, M., Building automated theorem provers for infinitely valued logics with satisfiability modulo theory solvers, IEEE 42nd International Symposium on Multiple-Valued Logic (ISMVL 2012), 15-30 (2013) |
| [6] | Baader, F.; Peñaloza, R., On the undecidability of fuzzy description logics with GCIs and product T-norm, Proceedings of the Frontiers of Combining Systems (FroCoS2011), 55-70 (2011), Springer · Zbl 1348.68236 |
| [7] | Barrett, C.; Stump, A.; Tinelli, C., The SMT-LIB Standard: Version 2.0, Technical Report (2010), Department of Computer Science, The University of Iowa |
| [9] | Bobillo, F.; Bou, F.; Straccia, U., On the failure of the finite model property in some fuzzy description logics, Fuzzy Sets Syst., 172, 1, 1-12 (2011) · Zbl 1231.03025 |
| [10] | Bobillo, F.; Cerami, M.; Esteva, F.; García-Cerdaña, A.; Peñaloza, R.; Straccia, U., Fuzzy description logics in the framework of mathematical fuzzy logic, (Cintula, R.; Cintula, P., Ch. 16 of Handbook of Mathematical Fuzzy Logic, Volume 3, volume 58 of Studies in Logic, Mathematical Logic and Foundations (2015)), 1105-1181 · Zbl 1436.03157 |
| [11] | Bobillo, F.; Straccia, U., fuzzyDL: an expressive fuzzy description logic reasoner, Proceedings of the IEEE World Congress on Computational Intelligence, 923-930 (2008) |
| [12] | Bobillo, F.; Straccia, U., Fuzzy description logics with general t-norms and datatypes, Fuzzy Sets Syst., 160, 23, 3382-3402 (2009) · Zbl 1192.68659 |
| [13] | Bobillo, F.; Straccia, U., The fuzzy ontology reasoner fuzzyDL, Knowl. Based Syst., 95, 12-34 (2016) |
| [14] | Bobillo, F.; Straccia, U., Optimising fuzzy description logic reasoners with general concept inclusion absorption, Fuzzy Sets Syst., 292, 98-129 (2016) · Zbl 1380.68351 |
| [15] | Bofill, M.; Manyà, F.; Vidal, A.; Villaret, M., The complexity of 3-valued łukasiewicz rules, Proceedings of the Modeling Decisions for Artificial Intelligence - 12th International Conference, MDAI 2015, Lecture Notes in Computer Science, 9321, 221-229 (2015), Springer · Zbl 1366.68086 |
| [16] | Bofill, M.; Manyà, F.; Vidal, A.; Villaret, M., Finding hard instances of satisfiability in lukasiewicz logics, Proceedings of the IEEE 45nd International Symposium on Multiple-Valued Logic (ISMVL), 30-35 (2015), IEEE CS Press |
| [17] | Bou, F.; Esteva, F.; Godo, L.; Rodríguez, R., On the minimum many-valued modal logic over a finite residuated lattice, J. Logic Comput., 21, 5, 739-790 (2011) · Zbl 1252.03040 |
| [18] | Caicedo, X.; Metcalfe, G.; Rodríguez, R.; Rogger, J., A finite model property for gödel modal logics, Proceedings of the 20th International Workshop, WoLLIC 2013, Logic, Language, Information, and Computation, vol. 8071, 226-237 (2013), Springer · Zbl 1395.03008 |
| [19] | Caicedo, X.; Rodriguez, R. O., Bi-modal Gödel logic over [0, 1]-valued kripke frames, J. Logic Comput., 25, 1, 37-55 (2015) · Zbl 1371.03035 |
| [20] | Caicedo, X.; Rodríguez, R. O., Standard Gödel modal logics, Studia Logica, 94, 2, 189-214 (2010) · Zbl 1266.03030 |
| [21] | Cerami, M.; Straccia, U., On the (un)decidability of fuzzy description logics under łukasiewicz t-norm, Inf. Sci., 227, 1-21 (2013) · Zbl 1293.68255 |
| [22] | Chagrov, A.; Zakharyaschev, M., Modal Logic (1997), Oxford University Press · Zbl 0871.03007 |
| [23] | Cignoli, R.; Torrens, A., An algebraic analysis of product logic, Multiple-Valued Logic, 5, 45-65 (2000) · Zbl 0962.03059 |
| [24] | Cintula, P.; Hájek, P.; Noguera, C., Handbook of Mathematical Fuzzy Logic, 2 volumes, volume 37 and 38 of Studies in Logic. Mathematical Logic and Foundation (2011), College Publications · Zbl 1283.03001 |
| [25] | de Moura, L. M.; Bjørner, N., Z3: An efficient SMT solver, Proceedings of Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the ETAPS 2008, 337-340 (2008), Springer |
| [26] | Hähnle, R., Automated deduction in multiple valued logics, volume 10 of International Series of Monographs on Computer Science (1993), The Clarendon Press Oxford University Press: The Clarendon Press Oxford University Press New York · Zbl 0798.03010 |
| [27] | Hájek, P., Metamathematics of fuzzy logic, volume 4 of Trends in Logic—Studia Logica Library (1998), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht · Zbl 0937.03030 |
| [28] | Hájek, P., Making fuzzy description logic more general, Fuzzy Sets Syst., 154, 1, 1-15 (2005) · Zbl 1094.03014 |
| [29] | Hansoul, G.; Teheux, B., Extending łukasiewicz logics with a modality: algebraic approach to relational semantics, Studia Logica, 101, 3, 505-545 (2013) · Zbl 1272.03100 |
| [30] | Montagna, F., Generating the variety of BL-algebras, Soft Comput., 9, 12, 869-874 (2005) · Zbl 1093.03039 |
| [31] | Mostert, P. S.; Shields, A. L., On the structure of semigroups on a compact manifold with boundary, Ann. Math., 65, 117-143 (1957), Second Series · Zbl 0096.01203 |
| [32] | de Moura, L.; Bjørner, N., Satisfiability modulo theories: introduction and applications, Commun. ACM, 54, 69-77 (2011) |
| [33] | Mundici, D., Satisfiability in many-valued sentential logic is NP-complete, Theor. Comput. Sci., 52, 1-2, 145-153 (1987) · Zbl 0639.03042 |
| [34] | Rothenberg, R., A class of theorems in Łukasiewicz logic for benchmarking automated theorem provers, (Olivetti, N., TABLEAUX ’07, Automated Reasoning with Analytic Tableaux and Related Methods, Position Papers (2007)), 101-111 |
| [35] | Schockaert, S.; Janssen, J.; Vermeir, D., Satisfiability checking in Łukasiewicz logic as finite constraint satisfaction, J. Autom. Reasoning, 49, 4, 493-550 (2012) · Zbl 1315.03035 |
| [36] | Schockaert, S.; Janssen, J.; Vermeir, D.; De Cock, M., Finite satisfiability in infinite-valued Łukasiewicz logic, proceedings of Scalable Uncertainty Management (SUM 2009), Lecture Notes in Computer Science, 5785, 240-254 (2009), Springer |
| [37] | Sebastiani, R., Lazy satisability modulo theories, J. Satisfiability Boolean Model.Comput., 3, 3-4, 141-224 (2007) · Zbl 1145.68501 |
| [38] | Straccia, U., Foundations of fuzzy logic and semantic web languages, Chapman & Hall CRC Studies in Informatics Series (2013) |
| [39] | Straccia, U., All about fuzzy description logics and applications, Reasoning Web, 11th International Summer School, Tutorial Lectures. Reasoning Web, 11th International Summer School, Tutorial Lectures, Lecture Notes in Computer Science, 9203, 1-31 (2015), Springer · Zbl 1358.68279 |
| [40] | Vidal, A.; Bou, F.; Godo, L., An SMT-based solver for continuous t-norm based logics, Proceedings of Scalable Uncertainty Management (SUM2012), Lecture Notes in Computer Science, 7520, 633-640 (2012), Springer |
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.
