Efficient representation of piecewise linear functions into Łukasiewicz logic modulo satisfiability. (English) Zbl 1512.68428
Summary: This work concerns the representation of a class of continuous functions into Logic, so that one may automatically reason about properties of these functions using logical tools. Rational McNaughton functions may be implicitly represented by logical formulas in Łukasiewicz Infinitely-valued Logic by constraining the set of allowed valuations; such a restriction contemplates only those valuations that satisfy specific formulas. This work investigates two approaches to such depiction, called representation modulo satisfiability. Furthermore, a polynomial-time algorithm that builds this representation is presented, producing a pair of formulas consisting of the representative formula and the constraining one, given as input a rational McNaughton function in a suitable encoding. An implementation of the algorithm is discussed.
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
| 03B35 | Mechanization of proofs and logical operations |
| 03B50 | Many-valued logic |
| 68W40 | Analysis of algorithms |
Keywords:
function representation; Łukasiewicz infinite-valued logic; rational McNaughton functions; piecewise linear functionsReferences:
| [1] | Aguzzoli, S. (1998). The complexity of McNaughton functions of one variable. Advances in Applied Mathematics21 (1) 58-77. · Zbl 0911.03004 |
| [2] | Aguzzoli, S. and Mundici, D. (2001). Weierstrass approximations by Łukasiewicz formulas with one quantified variable. In: Proceedings 31st IEEE International Symposium on Multiple-Valued Logic, IEEE, 361-366. |
| [3] | Aguzzoli, S. and Mundici, D. (2003). Weierstrass Approximation Theorem and Łukasiewicz Formulas with one Quantified Variable, Physica-Verlag HD, Heidelberg, 315-335. · Zbl 1046.03010 |
| [4] | Amato, P., Di Nola, A. and Gerla, B. (2002). Neural networks and rational Łukasiewicz logic. In: 2002 Annual Meeting of the North American Fuzzy Information Processing Society Proceedings. NAFIPS-FLINT 2002 (Cat. No. 02TH8622), IEEE, 506-510. |
| [5] | Amato, P. and Porto, M. (2000). An algorithm for the automatic generation of a logical formula representing a control law. Neural Network World10 (5) 777-786. |
| [6] | Ansótegui, C., Bofill, M., Manyà, F. and Villaret, M. (2012). Building automated theorem provers for infinitely-valued logics with satisfiability modulo theory solvers. In: 2012 IEEE 42nd International Symposium on Multiple-Valued Logic, 25-30. |
| [7] | Barrett, C., Fontaine, P. and Tinelli, C. (2016). The satisfiability modulo theories library (SMT-LIB). www.SMT-LIB.org. |
| [8] | Bertsimas, D. and Tsitsiklis, J. N. (1997). Introduction to Linear Optimization, Athena Scientific, Belmont, MA. |
| [9] | Bofill, M., Manya, F., Vidal, A. and Villaret, M. (2015). Finding hard instances of satisfiability in Łukasiewicz logics. In: 2015 IEEE International Symposium on Multiple-Valued Logic (ISMVL), IEEE, 30-35. |
| [10] | Cignoli, R., D’Ottaviano, I. and Mundici, D. (2000). Algebraic Foundations of Many-Valued Reasoning, Trends in Logic, Springer, Netherlands. · Zbl 0937.06009 |
| [11] | Di Nola, A. and Leuştean, I. (2011). Riesz MV-algebras and their logic. In: Proceedings of the 7th Conference of the European Society for Fuzzy Logic and Technology (EUSFLAT-11), Atlantis Press, 140-145. · Zbl 1254.06008 |
| [12] | Di Nola, A. and Leuştean, I. (2014). Łukasiewicz logic and Riesz spaces. Soft Computing182349-2363. |
| [13] | Dutertre, B. (2014). Yices 2.2. In: Biere, A. and Bloem, R. (eds.) Computer-Aided Verification (CAV’2014), Lecture Notes in Computer Science, vol. 8559, Springer, 737-744. |
| [14] | Esteva, F., Godo, L. and Montagna, F. (2001). The \(\unicode{x0141}\Pi\) and \(\unicode{x0141}\Pi\frac{1}{2}\) logics: Two complete fuzzy systems joining Łukasiewicz and product logics. Archive for Mathematical Logic40 (1) 39-67. · Zbl 0966.03022 |
| [15] | Finger, M. and Preto, S. (2018). Probably half true: Probabilistic satisfiability over Łukasiewicz infinitely-valued logic. In: Galmiche, D., Schulz, S. and Sebastiani, R. (eds.) Automated Reasoning, Cham, Springer International Publishing, 194-210. · Zbl 1468.68199 |
| [16] | Finger, M. and Preto, S. (2020). Probably partially true: Satisfiability for Łukasiewicz infinitely-valued probabilistic logic and related topics. Journal of Automated Reasoning64 (7) 1269-1286. · Zbl 1468.68200 |
| [17] | Gamrath, G., Anderson, D., Bestuzheva, K., Chen, W.-K., Eifler, L., Gasse, M., Gemander, P., Gleixner, A., Gottwald, L., Halbig, K., Hendel, G., Hojny, C., Koch, T., Bodic, P. L., Maher, S. J., Matter, F., Miltenberger, M., Mühmer, E., Müller, B., Pfetsch, M., Schlösser, F., Serrano, F., Shinano, Y., Tawfik, C., Vigerske, S., Wegscheider, F., Weninger, D. and Witzig, J. (2020). The SCIP optimization suite 7.0. Technical report, Optimization Online. |
| [18] | Gerla, B. (2001). Rational Łukasiewicz logic and DMV-algebras. Neural Network World11 (6) 579-594. |
| [19] | Leshno, M., Lin, V. Y., Pinkus, A. and Schocken, S. (1993). Multilayer feedforward networks with a nonpolynomial activation function can approximate any function. Neural Networks6 (6) 861-867. |
| [20] | Mcnaughton, R. (1951). A theorem about infinite-valued sentential logic. Journal of Symbolic Logic161-13. · Zbl 0043.00901 |
| [21] | Mundici, D. (1987). Satisfiability in many-valued sentential logic is NP-complete. Theoretical Computer Science52 (1-2) 145-153. · Zbl 0639.03042 |
| [22] | Mundici, D. (1994). A constructive proof of McNaughton’s theorem in infinite-valued logic. Journal of Symbolic Logic59 (2) 596-602. · Zbl 0807.03012 |
| [23] | Preto, S. and Finger, M. (2020). An efficient algorithm for representing piecewise linear functions into logic. Electronic Notes in Theoretical Computer Science 351 167-186. Proceedings of LSFA 2020, the 15th International Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2020). · Zbl 1498.03061 |
| [24] | Tarela, J., Alonso, E. and Martínez, M. (1990). A representation method for PWL functions oriented to parallel processing. Mathematical and Computer Modelling13 (10) 75-83. · Zbl 0723.68045 |
| [25] | Tarela, J. and Martínez, M. (1999). Region configurations for realizability of lattice piecewise-linear models. Mathematical and Computer Modelling30 (11-12) 17-27. · Zbl 1043.94552 |
| [26] | Xu, J. and Wang, S. (2019). Lattice piecewise affine representations on convex projection regions. In: 2019 IEEE 58th Conference on Decision and Control (CDC), 7240-7245. |
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.
