{"entities":{"Q6174545":{"pageid":13309433,"ns":120,"title":"Item:Q6174545","lastrevid":94155035,"modified":"2026-06-05T06:01:13Z","type":"item","id":"Q6174545","labels":{"en":{"language":"en","value":"Verifying feedforward neural networks for classification in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7728855"}},"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":"Q6174545$7065C455-CF54-4EDE-84C8-FE92D12CD5C6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a5285819c55eb22cd17db84678c1909f72922c21","datavalue":{"value":{"text":"Verifying feedforward neural networks for classification in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6174545$456E57A4-2564-45F7-9C66-C2E1E5927A4F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"10734f2fa8d4cf302b83e0eecfcedd3bbd4b2280","datavalue":{"value":"1529.68154","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6174545$52A157D0-DD20-4AC4-A224-1E3957CAF143","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ebb4810dee346d017aa91b211faca406d5286f0e","datavalue":{"value":"10.1007/978-3-031-27481-7_24","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6174545$646E77DE-88A0-4BCB-8319-F04E1C7B0318","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f5b3f2efcf958b40022b60d5ff3169a1615bdabb","datavalue":{"value":{"entity-type":"item","numeric-id":470023,"id":"Q470023"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174545$31B50DC8-68F4-428F-925F-237CF5274759","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3f5a5e7c8f47786302c18bb9a936da8d2d27fe38","datavalue":{"value":{"entity-type":"item","numeric-id":6174544,"id":"Q6174544"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174545$7C859669-26AD-4D17-AA8B-F4F9964FF9CE","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e94b967ae8cf6f3b704a08992f5caf4130874d09","datavalue":{"value":{"entity-type":"item","numeric-id":5918261,"id":"Q5918261"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174545$17BCD482-4313-4258-B502-7CF335329D3D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"441006eb796e3a3facfc20a479629ee7d34004ed","datavalue":{"value":{"time":"+2023-08-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6174545$94DD7CDF-B1D4-4372-96A7-687CEAFFEB8D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6174545$D2CF7F01-E9D3-4188-A825-8DC8408ABEE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"86ef24f5c9e2aac48660aa2e36054c8246d3fc97","datavalue":{"value":"68T07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6174545$710F10C7-5F37-41ED-89F2-81F993478F62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6174545$883C52EC-B698-43A3-AB46-D18D1074BD16","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ec90557a68fc3f9404f6e5a1fd63dbf8c39f931c","datavalue":{"value":"7728855","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6174545$37892F39-E749-4608-9B5B-1D2E4ED62C9C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"694eecdc2f71e4a898283c6db5c2b7894fc662da","datavalue":{"value":"neural network","type":"string"},"datatype":"string"},"type":"statement","id":"Q6174545$51228E90-C541-4A61-9DA8-C79496479B63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"977ed9a5dd338bf424fd0ab29d89678ee0103ad0","datavalue":{"value":"deep learning","type":"string"},"datatype":"string"},"type":"statement","id":"Q6174545$BA09C121-C037-4675-B30E-F8F4652BC567","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6fd29425aeabd18c7eef36a7784dcce837a8dc0f","datavalue":{"value":"classification network","type":"string"},"datatype":"string"},"type":"statement","id":"Q6174545$6E3266C7-F46A-43B6-A7B0-72206759F208","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7a4074c21e2e7511cbc10eeace46b2a5ff0a7e0a","datavalue":{"value":"feedforward network","type":"string"},"datatype":"string"},"type":"statement","id":"Q6174545$A09636F1-7D87-463A-AE0B-9D76CCED71C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66824d9cf653f7dee3c76f98a8ea1aa06432fa7c","datavalue":{"value":"verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q6174545$3BC7520E-98CD-4954-8732-CB18AD7CAA17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42f0513e500ea6cb630e73925875c7d53ca8d8e1","datavalue":{"value":"Isabelle/HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q6174545$CCF300BE-E022-494A-AEC1-138C5A7F70AD","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":"Q6174545$4FF981CE-DD40-4790-84CA-34735F79B686","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"94fe41a85a05383935c29ab90c4d3044c329de6e","datavalue":{"value":{"entity-type":"item","numeric-id":4569250,"id":"Q4569250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174545$B9804A27-DF2B-497D-9309-1F2A8D6782A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3d0530cff2ea3a00fdf0e71f199a08187bea8b91","datavalue":{"value":{"entity-type":"item","numeric-id":5096089,"id":"Q5096089"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174545$047D9881-1960-4F3B-9FC6-F41E821AE474","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0560d1c327ad31efacda0335b3172566e741ab91","datavalue":{"value":{"entity-type":"item","numeric-id":2151229,"id":"Q2151229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174545$B3047666-5E04-400E-8E08-467F1E67A24C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"09d76610be2db7a475aae1f8e37aec5be549c297","datavalue":{"value":{"entity-type":"item","numeric-id":2151238,"id":"Q2151238"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174545$89C18B26-8458-4825-AE3B-6195D44038AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7f1461786fd9147b7231c61e645f0ab20a3eaa42","datavalue":{"value":{"entity-type":"item","numeric-id":1040002,"id":"Q1040002"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174545$61E66332-F623-4B40-A5FB-11E83E202926","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d8a6a7f4a099b96912e5cba667c8ca70d007bb8","datavalue":{"value":{"entity-type":"item","numeric-id":287365,"id":"Q287365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174545$8E677FBF-1503-4481-B150-0DBE3606ED9A","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":"Q6174545$633E33AF-4370-4F9D-AA6D-F38037204E4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"085f2f402bb0aaa918a693e06aa64da16c2193f2","datavalue":{"value":{"entity-type":"item","numeric-id":5687569,"id":"Q5687569"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174545$91D0D258-253F-4824-912F-B9CD557015F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c48cc560b409d49a8557b49c60f6d76bde09c8f","datavalue":{"value":{"entity-type":"item","numeric-id":5354403,"id":"Q5354403"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174545$AAB253E3-8E7A-4BDC-92C3-DD09EFC6616B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a11ebadcb58c67798856970cbffd1e7880f49d5","datavalue":{"value":{"entity-type":"item","numeric-id":6109579,"id":"Q6109579"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174545$98CA72CF-4CF6-4065-9249-6E24734C8F04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6a3f0c070d63cc8ade73e849526c8ff12c4b898b","datavalue":{"value":{"entity-type":"item","numeric-id":3523187,"id":"Q3523187"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6174545$4FE4E1AB-C8BF-432C-B162-672DEAEC9E15","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6db2590a686e2cd107be2bfb07bc1026cc813b3b","datavalue":{"value":{"entity-type":"item","numeric-id":5096089,"id":"Q5096089"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"08d3c05f49eb237b47d9745b0c58eb816ce897c4","datavalue":{"value":{"amount":"+0.7784147262573242","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":"Q6174545$2D7E3316-FE8D-45C1-99D8-3DBAE52DD49A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ef5e9575d3f99653ee212b6198623fb0a9530c0d","datavalue":{"value":{"entity-type":"item","numeric-id":2151229,"id":"Q2151229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a2d72b8e02ef11e2a98d75997fc6af80054e3d67","datavalue":{"value":{"amount":"+0.7683418989181519","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":"Q6174545$CC68A530-A2ED-4992-B677-FC4725B098C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1764a65cb4a07d5e7c4470ac49751b042722d8e8","datavalue":{"value":{"entity-type":"item","numeric-id":6109579,"id":"Q6109579"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9826ae101f0840ad509ac64da1e607d52be1a14e","datavalue":{"value":{"amount":"+0.7620836496353149","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":"Q6174545$3458AE9C-86E6-418B-AA97-0D38BA00ECE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"80c35f16574fc06d6eccd38fbf10b4591d2b7727","datavalue":{"value":{"entity-type":"item","numeric-id":6108442,"id":"Q6108442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2b21e1c958ff460e825338a69afef80a923c3393","datavalue":{"value":{"amount":"+0.7165094017982483","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":"Q6174545$7050D7CB-6424-4705-83A6-633664FBA8A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"85cea1ff044ff4cce339eeeecb38788d5dffa57e","datavalue":{"value":{"entity-type":"item","numeric-id":2145326,"id":"Q2145326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"16be64025d7174fc98dc500d6510d04c6817bdc5","datavalue":{"value":{"amount":"+0.7068924307823181","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":"Q6174545$CFEF881B-96C9-455F-8012-CFFB184F2788","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Verifying feedforward neural networks for classification in Isabelle/HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Verifying_feedforward_neural_networks_for_classification_in_Isabelle/HOL"}}}}}