{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,12]],"date-time":"2025-10-12T02:12:03Z","timestamp":1760235123274,"version":"build-2065373602"},"reference-count":30,"publisher":"MDPI AG","issue":"8","license":[{"start":{"date-parts":[[2021,7,30]],"date-time":"2021-07-30T00:00:00Z","timestamp":1627603200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61772006"],"award-info":[{"award-number":["61772006"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Information"],"abstract":"<jats:p>Error coefficients are ubiquitous in systems. In particular, errors in reasoning verification must be considered regarding safety-critical systems. We present a reasoning method that can be applied to systems described by the polynomial error assertion (PEA). The implication relationship between PEAs can be converted to an inclusion relationship between zero sets of PEAs; the PEAs are then transformed into first-order polynomial logic. Combined with the quantifier elimination method, based on cylindrical algebraic decomposition, the judgment of the inclusion relationship between zero sets of PEAs is transformed into judgment error parameters and specific error coefficient constraints, which can be obtained by the quantifier elimination method. The proposed reasoning method is validated by proving the related theorems. An example of intercepting target objects is provided, and the correctness of our method is tested through large-scale random cases. Compared with reasoning methods without error semantics, our reasoning method has the advantage of being able to deal with error parameters.<\/jats:p>","DOI":"10.3390\/info12080309","type":"journal-article","created":{"date-parts":[[2021,7,30]],"date-time":"2021-07-30T12:59:24Z","timestamp":1627649964000},"page":"309","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Reasoning Method between Polynomial Error Assertions"],"prefix":"10.3390","volume":"12","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4784-8984","authenticated-orcid":false,"given":"Peng","family":"Wu","sequence":"first","affiliation":[{"name":"School of Computer and Information Technology, Beijing Jiaotong University, Beijing 100044, China"},{"name":"School of Innovation, Design and Engineering, M\u00e4lardalen University, 72123 V\u00e4ster\u00e5s, Sweden"}]},{"given":"Ning","family":"Xiong","sequence":"additional","affiliation":[{"name":"School of Innovation, Design and Engineering, M\u00e4lardalen University, 72123 V\u00e4ster\u00e5s, Sweden"}]},{"given":"Juxia","family":"Xiong","sequence":"additional","affiliation":[{"name":"School of Mathematics and Physics, Guangxi University for Nationalities, Nanning 530006, China"}]},{"given":"Jinzhao","family":"Wu","sequence":"additional","affiliation":[{"name":"School of Computer and Information Technology, Beijing Jiaotong University, Beijing 100044, China"},{"name":"School of Mathematics and Physics, Guangxi University for Nationalities, Nanning 530006, China"}]}],"member":"1968","published-online":{"date-parts":[[2021,7,30]]},"reference":[{"key":"ref_1","unstructured":"Clarke, E.M., Grumberg, O., and Peled, D. (1999). Model Checking, MIT Press."},{"key":"ref_2","unstructured":"Doyen, L., Frehse, G., and Pappas, G.J. (2018). Handbook of Model Checking, Springer International Publishing."},{"key":"ref_3","first-page":"300","article-title":"First-order logic and automated theorem proving","volume":"61","author":"Fitting","year":"1998","journal-title":"Studia Log."},{"key":"ref_4","first-page":"1","article-title":"Combining theorem proving and model checking through symbolic analysis","volume":"1877","author":"Shankar","year":"2000","journal-title":"Int. Conf. Concurr. Theory."},{"key":"ref_5","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/10720084_11","article-title":"Combinations of model checking and theorem proving","volume":"Volume 1794","author":"Uribe","year":"2000","journal-title":"Proceedings of the International Workshop on Frontiers of Combining Systems"},{"key":"ref_6","doi-asserted-by":"crossref","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","article-title":"A survey of automated techniques for formal software verification","volume":"27","author":"Kroening","year":"2008","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"ref_7","doi-asserted-by":"crossref","unstructured":"Sun, T., and Yu, W.A. (2020). Formal Verification Framework for Security Issues of Blockchain Smart Contracts. Electronics, 9.","DOI":"10.3390\/electronics9020255"},{"key":"ref_8","unstructured":"Kaufmann, D. (2020). Formal Verification of Multiplier Circuits Using Computer Algebra. [Ph.D. Thesis, Johannes Kepler University Linz]."},{"key":"ref_9","doi-asserted-by":"crossref","first-page":"615","DOI":"10.1007\/11498490_29","article-title":"Labelled transition systems","volume":"Volume 3472","author":"Katoen","year":"2005","journal-title":"Lecture Notes in Computer Science"},{"key":"ref_10","first-page":"773","article-title":"Algebraic methods for mechanical theorem proving in many-valued logics","volume":"10","author":"Wu","year":"1996","journal-title":"Chin. J. Comput."},{"key":"ref_11","doi-asserted-by":"crossref","unstructured":"Fu, J., Wu, J., and Tan, H. (2015). A deductive approach towards reasoning about algebraic transition systems. Math. Probl. Eng., 607013.","DOI":"10.1155\/2015\/607013"},{"key":"ref_12","doi-asserted-by":"crossref","unstructured":"Platzer, A. (2010). Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics, Springer Science & Business Media.","DOI":"10.1007\/978-3-642-14509-4"},{"key":"ref_13","doi-asserted-by":"crossref","unstructured":"Platzer, A. (2012, January 13\u201315). A differential operator approach to equational differential invariants. Proceedings of the International Conference on Interactive Theorem Proving, Princeton, NJ, USA.","DOI":"10.1007\/978-3-642-32347-8_3"},{"key":"ref_14","unstructured":"Chakraborty, S., Jerraya, A., Baruah, S.K., and Fischmeister, S. (2011, January 9\u201314). Computing semi-algebraic invariants for polynomial dynamical systems. Proceedings of the Ninth ACM International Conference on Embedded Software, Taipei, Taiwan."},{"key":"ref_15","doi-asserted-by":"crossref","unstructured":"He, H., and Wu, J. (2020). A New Approach to Nonlinear Invariants for Hybrid Systems Based on the Citing Instances Method. Information, 11.","DOI":"10.3390\/info11050246"},{"key":"ref_16","doi-asserted-by":"crossref","unstructured":"Rushby, J. (2000). Theorem proving for verification. Summer School on Modeling and Verification of Parallel Processes, Springer.","DOI":"10.1007\/3-540-45510-8_2"},{"key":"ref_17","doi-asserted-by":"crossref","unstructured":"Chen, Z., Zhang, T., and Li, Z. (2017, January 26\u201327). Hybrid Control Scheme Consisting of Adaptive and Optimal Controllers for Flexible-Base Flexible-Joint Space Manipulator with Uncertain Parameters. Proceedings of the 9th International Conference on Intelligent Human-Machine Systems and Cybernetics (IHMSC), Hangzhou, China.","DOI":"10.1109\/IHMSC.2017.84"},{"key":"ref_18","doi-asserted-by":"crossref","first-page":"47384","DOI":"10.1109\/ACCESS.2020.2979352","article-title":"Adaptive disturbance attenuation control of two tank liquid level system with uncertain parameters based on port-controlled Hamiltonian","volume":"8","author":"Xu","year":"2020","journal-title":"IEEE Access"},{"key":"ref_19","doi-asserted-by":"crossref","unstructured":"Wu, P., Xiong, N., Liu, J., Huang, L., Ju, Z., Ji, Y., and Wu, J. (2021). Interval Number-Based Safety Reasoning Method for Verification of Decentralized Power Systems in High-Speed Trains. Math. Probl. Eng., 6624528.","DOI":"10.1155\/2021\/6624528"},{"key":"ref_20","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1016\/j.knosys.2016.09.023","article-title":"Uncertain multi-attributes decision making method based on interval number with probability distribution weighted operators and stochastic dominance degree","volume":"113","author":"Wu","year":"2016","journal-title":"Knowl. Based Syst."},{"key":"ref_21","doi-asserted-by":"crossref","first-page":"4025","DOI":"10.1109\/TCYB.2016.2594491","article-title":"Limited rationality and its quantification through the interval number judgments with permutations","volume":"47","author":"Liu","year":"2017","journal-title":"IEEE Trans. Cybern."},{"key":"ref_22","unstructured":"Pae, S.-i., and Park, H. (2005, January 8\u201310). Solving parametric semi-algebraic systems. Proceedings of the 7th Asian Symposium on Computer Mathematics, Seoul, Korea."},{"key":"ref_23","doi-asserted-by":"crossref","unstructured":"Tarski, A. (1951). A Decision Method for Elementary Algebra and Geometry, University of California Press.","DOI":"10.1525\/9780520348097"},{"key":"ref_24","doi-asserted-by":"crossref","first-page":"865","DOI":"10.1137\/0213054","article-title":"Cylindrical algebraic decomposition. I. The basic algorithm","volume":"13","author":"Arnon","year":"1984","journal-title":"SIAM J. Comput."},{"key":"ref_25","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1145\/1358190.1358197","article-title":"DISCOVERER: A tool for solving semi-algebraic systems","volume":"41","author":"Xia","year":"2007","journal-title":"ACM Commun. Comput. Algebra."},{"key":"ref_26","doi-asserted-by":"crossref","first-page":"3894","DOI":"10.1002\/aic.16207","article-title":"Analytical and triangular solutions to operational flexibility analysis using quantifier elimination","volume":"64","author":"Zhao","year":"2018","journal-title":"AIChE J."},{"key":"ref_27","doi-asserted-by":"crossref","unstructured":"Vo\u00dfwinkel, R., Robenac, K., and Bajcinca, N. (2018, January 29). Input-to-State Stability Mapping for Nonlinear Control Systems Using Quantifier Elimination. Proceedings of the European Control Conference (ECC), Limassol, Cyprus.","DOI":"10.23919\/ECC.2018.8550228"},{"key":"ref_28","doi-asserted-by":"crossref","unstructured":"Mulligan, C., Davenport, J., and England, M. (2018). TheoryGuru: A Mathematica package to apply quantifier elimination technology to economics. International Congress on Mathematical Software, South Bend, IN, USA, 24\u201327 July 2018, Springer.","DOI":"10.1007\/978-3-319-96418-8_44"},{"key":"ref_29","doi-asserted-by":"crossref","unstructured":"Tonks, Z. (2020). A Poly-algorithmic Quantifier Elimination Package in Maple. Maple in Mathematics Education and Research, Springer International Publishing.","DOI":"10.1007\/978-3-030-41258-6_13"},{"key":"ref_30","unstructured":"Wang, Y. (2019). Error Evaluation Method and Robustness Analysis of Fuzzy Reasoning. [Ph.D. Thesis, Zhejiang Sci-Tech University]."}],"container-title":["Information"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2078-2489\/12\/8\/309\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T06:37:20Z","timestamp":1760164640000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2078-2489\/12\/8\/309"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,7,30]]},"references-count":30,"journal-issue":{"issue":"8","published-online":{"date-parts":[[2021,8]]}},"alternative-id":["info12080309"],"URL":"https:\/\/doi.org\/10.3390\/info12080309","relation":{},"ISSN":["2078-2489"],"issn-type":[{"type":"electronic","value":"2078-2489"}],"subject":[],"published":{"date-parts":[[2021,7,30]]}}}