{"entities":{"Q478381":{"pageid":480148,"ns":120,"title":"Item:Q478381","lastrevid":62129784,"modified":"2026-04-11T03:58:25Z","type":"item","id":"Q478381","labels":{"en":{"language":"en","value":"Verification and code generation for invariant diagrams in Isabelle"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6376568"}},"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":"Q478381$4EF9ABC4-D493-4A23-A70D-7B68600857B8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0873bb37b08f087e0bb25e86420ad6d6a482114e","datavalue":{"value":{"text":"Verification and code generation for invariant diagrams in Isabelle","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q478381$C046969B-096D-4999-AC24-91490B1B6668","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5e25ab78e7b42e5f0703a26782e09e43d3b30fa8","datavalue":{"value":"1304.68032","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q478381$FBE6C8D3-BA6E-4C7F-A8C6-08851EA71CDD","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"03dd836c35062b353c773aa5bb9f8bbbab8cff00","datavalue":{"value":{"entity-type":"item","numeric-id":432147,"id":"Q432147"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q478381$C817003D-FA3E-494D-A7DD-4F1CC929F932","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f7d76bab915fa5b11ba4114aa1f83889a977dcb6","datavalue":{"value":{"entity-type":"item","numeric-id":204599,"id":"Q204599"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q478381$40D3471F-3B60-4AA3-ABEE-D6B806BA24FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ee6bc9976a4982590f6fda988ddf49a6b773b345","datavalue":{"value":{"entity-type":"item","numeric-id":478380,"id":"Q478380"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q478381$CC24A157-7162-4240-80CC-DCC64BC61F35","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"2532b82fbfd494721e144e8b872f80867d7316e9","datavalue":{"value":{"entity-type":"item","numeric-id":246441,"id":"Q246441"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q478381$07302618-C14F-4DF8-B2C0-4D237E884D3A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"726f2859ee2ab0ef37011c240f51f25426a8471d","datavalue":{"value":{"time":"+2014-12-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q478381$0AE3A4F4-AF27-4587-90E9-EE4DEDB9CDEE","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q478381$98AC9CE6-CA4E-49F1-B723-17B4F96848A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q478381$5EC79EEB-FEB0-446F-ABE2-D9424CEE504D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q478381$1DC38D0D-F894-4E96-8305-06EA7AB2643C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a53a62c136e7cf1e9d3ca7f7eca4297f23ab6866","datavalue":{"value":"6376568","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q478381$BB7E8D07-82F1-466F-BCC5-5957AD82C099","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b6a9e72f52baf14d87dedb3700df5d6d0d3d0434","datavalue":{"value":"invariant-based programming","type":"string"},"datatype":"string"},"type":"statement","id":"Q478381$4A8D4281-995C-49EF-8B75-05A451852903","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bce10e56da58e5f43da3eb3f01abc10ede5ccd09","datavalue":{"value":"invariant diagrams","type":"string"},"datatype":"string"},"type":"statement","id":"Q478381$1AF90EC9-74B4-4247-9C86-6E7BA07CCD10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c466a31828be4527e6fa92732efebe73d5786789","datavalue":{"value":"verification conditions","type":"string"},"datatype":"string"},"type":"statement","id":"Q478381$1FEF0171-79E4-449D-817C-5C7974066866","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fa2f9e456b885388846d1e0014f0bb89be592959","datavalue":{"value":"Isabelle proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q478381$8FEB020C-AD88-4D04-A1E9-E216006FBCE8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f9ac4ef6ef6c5f8856ee80195276e724e0b6225a","datavalue":{"value":"correctness","type":"string"},"datatype":"string"},"type":"statement","id":"Q478381$479780C5-155B-413E-B59B-F743E641BF13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c92f25b9ea895f2b57606a79389bb66216727043","datavalue":{"value":"recursive functions","type":"string"},"datatype":"string"},"type":"statement","id":"Q478381$87E4DBEB-6B61-4D5D-90A5-F85C02CF8FAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d62798ced101241ac0d5e46110e32d69e73a0c1a","datavalue":{"value":"proof automation","type":"string"},"datatype":"string"},"type":"statement","id":"Q478381$037F277C-4521-48EA-86EB-96A385C3B9AC","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4c394b74049cbdb0cef88807aac9fa3513bba728","datavalue":{"value":{"entity-type":"item","numeric-id":13169,"id":"Q13169"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q478381$1547629A-CAAC-431A-9066-C3C5B5211990","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q478381$7CF02177-0A63-4B81-B3DE-BFD0DB24E884","rank":"normal"},{"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":"Q478381$C54A5608-D133-475E-97A7-8DC40E438FA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9b0860d94af5fdff4b5635709ae334aacdf07ca1","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q478381$C85788EA-7F69-421A-9B59-F3985CEECCED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2ad21f150c621099eebc7c2e673cd9cf43b81a4e","datavalue":{"value":{"entity-type":"item","numeric-id":24376,"id":"Q24376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q478381$B0FFC2FC-EA6E-4869-813F-6D496FEF8F71","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":"Q478381$20E7AE86-0741-4BD9-9337-569037CB567E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6bf6b022cdaca4448ef36661ed178fefdc7609d9","datavalue":{"value":"https://doi.org/10.1016/j.jlap.2013.09.001","type":"string"},"datatype":"url"},"type":"statement","id":"Q478381$66FE2BA3-7C86-44F1-B160-94000193CFDB","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a51141032c182a0a1b938e85e4943a4044ab8788","datavalue":{"value":"W2029872263","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q478381$FE2F53CC-B05A-43F0-9DAB-3F0204B11A0F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"4d563b33a97ae532ceb4fa7611f2c0c8a02aa021","datavalue":{"value":{"entity-type":"item","numeric-id":1019025,"id":"Q1019025"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q478381$93980B12-A5AD-43D9-8232-8F9B270645F9","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":"Q478381$77BE473D-7CAE-4AA9-9D7D-7B5B0C526436","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c39b9040e3d2807bc13175b6074f0175a0a4a1c","datavalue":{"value":{"entity-type":"item","numeric-id":5747754,"id":"Q5747754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q478381$B05880A3-9792-410E-BB23-83D2DCF29479","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"931c42c28f22f89fe1b66164f9ececc2021ac1a2","datavalue":{"value":{"entity-type":"item","numeric-id":3558332,"id":"Q3558332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q478381$B72D4431-5160-4894-9B83-CB16AED9AACE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8814f08a007eccd0762345bdf06bc2170a9f2f1b","datavalue":{"value":{"entity-type":"item","numeric-id":2655335,"id":"Q2655335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q478381$66B2EDA0-C152-46FC-9742-2AFE423A484A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"211eb911509defcf3cc735956cc564f8ce863a20","datavalue":{"value":{"entity-type":"item","numeric-id":4809043,"id":"Q4809043"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q478381$D8328ED3-758D-450C-B227-01EF9FCB39E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5f6791f3e085b5e70981abdc04d407a28ff0f651","datavalue":{"value":{"entity-type":"item","numeric-id":5168887,"id":"Q5168887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q478381$5D2EC386-12EB-4363-8CFB-AAA2F4C22F33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98052a8fe89669b2fe4131e688755f41384ea6a6","datavalue":{"value":{"entity-type":"item","numeric-id":5178875,"id":"Q5178875"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q478381$2A663304-1768-48C2-B93C-E54CF97CED19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a655377852f4fbc1e40cdceec18686655bda680","datavalue":{"value":{"entity-type":"item","numeric-id":5712320,"id":"Q5712320"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q478381$28BB80FA-18FD-46CB-884F-53A4E1284621","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7adbd8b01f2575db09ed121ee5b9ac87e370daec","datavalue":{"value":"10.1016/J.JLAP.2013.09.001","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q478381$37A2BBCD-21BF-4104-9A95-29580C8EBCB3","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"64e8e04ed04b7797d2d328dfe86ff8cf293f2492","datavalue":{"value":{"entity-type":"item","numeric-id":1019025,"id":"Q1019025"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dabe98c7cb431134faa1a4a2a3bd9fcdfce820f5","datavalue":{"value":{"amount":"+0.7876566052436829","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":"Q478381$08C15FFA-8753-4F80-8459-9030DC4CAB88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ac6e70bbf8188afda314c0541daddd9c43137063","datavalue":{"value":{"entity-type":"item","numeric-id":432148,"id":"Q432148"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4f27d51af943c38faac66ce08bab82945523aee3","datavalue":{"value":{"amount":"+0.7634900808334351","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":"Q478381$9481134E-42E2-4955-8E7C-1807C51FDB3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1c8b9f7343efe63e57ddd2bd2ef0ae5831271484","datavalue":{"value":{"entity-type":"item","numeric-id":2324018,"id":"Q2324018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"35c9aac242620de5e5e88878818cebf7e48ecc52","datavalue":{"value":{"amount":"+0.7034072279930115","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":"Q478381$2C5B21E3-E7B6-4BA2-BF89-8A44C9F26DE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cd22d3506c673255f8a54ba91ef67c56d97fc42f","datavalue":{"value":{"entity-type":"item","numeric-id":2754111,"id":"Q2754111"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"001dc885fff7af9c8df991b8beb7ceeb5c6eb389","datavalue":{"value":{"amount":"+0.6935199499130249","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":"Q478381$125679F1-234C-46A7-9A16-7777656B7AD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1ddfe8706eb56f964bdfd12380be6a420c1d49e0","datavalue":{"value":{"entity-type":"item","numeric-id":3543655,"id":"Q3543655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4c791f1ffecfc497d135469883f0908d055ce6c9","datavalue":{"value":{"amount":"+0.6928980350494385","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":"Q478381$17024A8E-7DDF-47E8-A288-81A1BF7ED9BB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Verification and code generation for invariant diagrams in Isabelle","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Verification_and_code_generation_for_invariant_diagrams_in_Isabelle"}}}}}