{"entities":{"Q2294128":{"pageid":2304871,"ns":120,"title":"Item:Q2294128","lastrevid":78556424,"modified":"2026-05-06T11:52:41Z","type":"item","id":"Q2294128","labels":{"en":{"language":"en","value":"Formalization of function matrix theory in HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7165622"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2294128$12A3FBD3-3B6F-4246-BA06-59CE3FDB19D6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7a46b2ea9e7f40c4457e53be95b7921a62ed46b8","datavalue":{"value":{"text":"Formalization of function matrix theory in HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2294128$BAE6ECE8-B9AE-4D18-9E19-10D9CD17331D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"da922e11ceb2f914d05b953a781a75c2149f4d24","datavalue":{"value":"1442.68258","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2294128$5471F478-BA40-46A4-81B8-8222B365C3D4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"29b0993e4977b224331cb73abef32f93c2e1dc5c","datavalue":{"value":"10.1155/2014/201214","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2294128$D780189C-775B-494C-9D23-51846EA1BD75","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fb41e43426ff3ff3f8a93f102f45b1fd00efc7eb","datavalue":{"value":{"entity-type":"item","numeric-id":826357,"id":"Q826357"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2294128$66CAED2D-9134-400C-AA01-062322A38D5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bad697f6be27ac07cc0bac5f2074dc40ed884baf","datavalue":{"value":{"entity-type":"item","numeric-id":258539,"id":"Q258539"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2294128$FB3FBAB2-83A2-4D64-9943-CBA78FD81199","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8d0d64bff6a234e8e185575f6c485fb374ee059c","datavalue":{"value":{"entity-type":"item","numeric-id":2294127,"id":"Q2294127"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2294128$25D33D46-8E0D-4F30-9395-2B4699C60E15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d39b4536ab4b3691fa10e20a21c234518780f867","datavalue":{"value":{"entity-type":"item","numeric-id":1665985,"id":"Q1665985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2294128$5F26AEE4-C92F-4F10-8A8A-A9D7118B7655","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ceeeb03fb5bd35f76f74e037e926f9b1ddfa2ff7","datavalue":{"value":{"entity-type":"item","numeric-id":1665986,"id":"Q1665986"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2294128$09363367-0851-4620-827B-336D92259A73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"104098849fe9397bbec83ba6f6e8db26016c555e","datavalue":{"value":{"entity-type":"item","numeric-id":1640129,"id":"Q1640129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2294128$D57F0F83-6613-486E-9E89-5C14BD69E48B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"bb299feb2b87699ac8beef494c52fd2765eaf609","datavalue":{"value":{"entity-type":"item","numeric-id":118601,"id":"Q118601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2294128$3DB3860D-02FF-4EC9-A7F2-8B831DCB2160","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c81b0ff7a16cf5dd5907466303464ced8542d6d2","datavalue":{"value":{"time":"+2020-02-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2294128$6177AC5B-C597-4E75-9DA8-24AB9E0DD245","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"0b3071375d46a0654c41e7364eeb20584cd3960d","datavalue":{"value":"Summary: Function matrices, in which elements are functions rather than numbers, are widely used in model analysis of dynamic systems such as control systems and robotics. In safety-critical applications, the dynamic systems are required to be analyzed formally and accurately to ensure their correctness and safeness. Higher-order logic (HOL) theorem proving is a promise technique to match the requirement. This paper proposes a higher-order logic formalization of the function vector and the function matrix theories using the HOL theorem prover, including data types, operations, and their properties, and further presents formalization of the differential and integral of function vectors and function matrices. The formalization is implemented as a library in the HOL system. A case study, a formal analysis of differential of quadratic functions, is presented to show the usefulness of the proposed formalization.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2294128$A8258DA3-229B-4A84-9E5E-3D69B390E4BB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2294128$31849A59-C49A-44CB-AD6D-0113EE41AB7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9d105b80ed6a98c28f7c2120246154d24eaf80df","datavalue":{"value":"15A54","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2294128$86EE4DB7-1A53-44EE-91A0-A6748918FE4E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"505ffb4e89f662de9eda296559718609c5dfa690","datavalue":{"value":"7165622","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2294128$4BC9026F-6741-4EB7-A55F-DAB5431BB52E","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"8b3989736d3fba14f78393153f5004c5821aee71","datavalue":{"value":"Q59050246","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2294128$94FEAFDB-D7CB-4B85-BC48-38BC2439999C","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2294128$59E868BD-5D67-4CB7-AFE5-69338860A6C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2294128$21C40E04-9B33-47E1-AE2A-FECB75DE4361","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"66eb045e037081b6f6e8499f9fef44d8fbb7e0b0","datavalue":{"value":{"entity-type":"item","numeric-id":22240,"id":"Q22240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2294128$973C0756-E322-4839-9DD1-DC06E1A333ED","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2294128$2739CAA5-AABD-44D8-AE68-ED349C4C9793","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ea137e8db4b93a0d555acb9635b183993a5705b9","datavalue":{"value":"https://doi.org/10.1155/2014/201214","type":"string"},"datatype":"url"},"type":"statement","id":"Q2294128$27A36FD6-FD0B-405A-B8C1-3B9571640BDB","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f3fb3f3c07fc2365e75849d259e2eb9aeed2dd9c","datavalue":{"value":"W1992678654","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2294128$8FA5E80D-65AD-4D2A-8DF1-E8B4ED3ED11A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"96536a3513c764186ae19524652263bcfe7ab572","datavalue":{"value":{"entity-type":"item","numeric-id":3163886,"id":"Q3163886"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2294128$C91BAC6B-4779-44D3-BCF2-9A8E2766CDC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"12a2c6e3b76030407fa04184ca51530b04ec3f06","datavalue":{"value":{"entity-type":"item","numeric-id":541222,"id":"Q541222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2294128$4694F6E1-C636-4E99-9E46-B1E353EC4AD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db34cad8e2582cb97143bb7413e549955629d3b2","datavalue":{"value":{"entity-type":"item","numeric-id":2392414,"id":"Q2392414"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2294128$D824C27C-8B89-4A01-9902-407AA8A24FD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a5a381aea19de04670d7853e3f88b0097bec6ffa","datavalue":{"value":{"entity-type":"item","numeric-id":3582709,"id":"Q3582709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2294128$36FA2BCA-9CD3-4B37-B421-15D6D1F6E2B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a5e182d22cd63374751049cb1ad374f0b5175f7","datavalue":{"value":{"entity-type":"item","numeric-id":5477650,"id":"Q5477650"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2294128$58BF21BF-7115-4A22-831C-773A9AA7A4C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2294128$72CDFB45-D7AC-4AFF-890C-B452B4D8DF18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cdfc7d5ee1b035b8d37b2573bd54cb7b24ba6f2d","datavalue":{"value":{"entity-type":"item","numeric-id":2379683,"id":"Q2379683"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2294128$9569E420-ED8F-4D6B-8217-18A075CE3A50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f81f950b10cba627720e02347cb540992691eba3","datavalue":{"value":{"entity-type":"item","numeric-id":5477658,"id":"Q5477658"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2294128$7BA04A0D-505C-48C0-8F7E-47F3B71B6EAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0a2e9b784de40e604d71aae31dafc097b629058","datavalue":{"value":{"entity-type":"item","numeric-id":2375421,"id":"Q2375421"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2294128$CF716310-34A7-4F3F-82B9-216DDB4D720E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6d7b6db4bf1924f8f4a4c27ad57224e0a8f56529","datavalue":{"value":{"entity-type":"item","numeric-id":2423767,"id":"Q2423767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"61210bed8baea4593b85d7fbc8a10c586290fbda","datavalue":{"value":{"amount":"+0.7915967702865601","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2294128$11A20058-D4AB-4AF1-9315-1F53E52564E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"895f01dbe4514afaf4e58308193c557e5a7e265f","datavalue":{"value":{"entity-type":"item","numeric-id":2375439,"id":"Q2375439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4ae1ea676dbbd544dfc63d5f0f1625858846dd0c","datavalue":{"value":{"amount":"+0.7488420009613037","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2294128$13A33EEB-3AF8-49D0-8A5C-D2D9E0826221","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e11c84bf77282e1f1f0c8baf716f17fa923785c4","datavalue":{"value":{"entity-type":"item","numeric-id":5495918,"id":"Q5495918"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8cd98f0a967b08f9b9d6bee13ebe6715185b483b","datavalue":{"value":{"amount":"+0.7485611438751221","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2294128$DCE8FE63-4283-4892-8854-F5640E47C170","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cd44137ac394e1796bfee579214b7e8724aec52c","datavalue":{"value":{"entity-type":"item","numeric-id":5119159,"id":"Q5119159"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"699d9dd1f3b2534ccb83a9441a7b0f4d7624bfa6","datavalue":{"value":{"amount":"+0.7448490262031555","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2294128$44404E9B-0D12-4059-9333-1FF2965CE365","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"51b4c1a6cc73475e4d910067ec5b89bfb7daced5","datavalue":{"value":{"entity-type":"item","numeric-id":2829282,"id":"Q2829282"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"31c6028d88808afb2a300305277c958481cf45a9","datavalue":{"value":{"amount":"+0.7383689284324646","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2294128$50F058C0-DECC-4E2D-AD7A-60EDE67CDFA4","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"daf5f856a5d861312ad309ab567540337a5f61d6","datavalue":{"value":{"entity-type":"item","numeric-id":57050,"id":"Q57050"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2294128$04A17499-3DD7-46BC-88FF-239522A53B58","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formalization of function matrix theory in HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formalization_of_function_matrix_theory_in_HOL"}}}}}