{"entities":{"Q1019024":{"pageid":1020872,"ns":120,"title":"Item:Q1019024","lastrevid":69431097,"modified":"2026-04-13T06:57:09Z","type":"item","id":"Q1019024","labels":{"en":{"language":"en","value":"The RISC ProofNavigator: a proving assistant for program verification in the classroom"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5558120"}},"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":"Q1019024$CF727BAF-D4CD-42F3-9A11-6F325478F7BE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9885eb536ee08b3897cb69e464c074ab8fa85963","datavalue":{"value":{"text":"The RISC ProofNavigator: a proving assistant for program verification in the classroom","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1019024$87A5E3B8-8A89-4A84-A4CB-AC30DCBFED19","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"eaa0d2ee2f721bd37f6dd9ec4751334e2078e857","datavalue":{"value":"1162.68478","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1019024$25C3069D-9562-442A-A142-D3CA23C9C2AC","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"bb33d69587ad5a852773f2fc55274bf330026170","datavalue":{"value":{"entity-type":"item","numeric-id":1019023,"id":"Q1019023"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1019024$716DE947-F964-4CC7-B669-001BA85821C6","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d9925518446645d219093152a820aba790417b61","datavalue":{"value":{"entity-type":"item","numeric-id":164203,"id":"Q164203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1019024$28C0EA89-B7D2-4743-B05F-86CB2451932E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9ce65d071e7340c2588abccb76c05f02030105cc","datavalue":{"value":{"time":"+2009-05-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1019024$4685533A-E763-4624-85B8-897D63D8F601","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1019024$6F397889-BCE8-43FD-A97E-D63A06CD1C66","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"759a99c2d08ef4a2dba27d347ca82bb5d10c2500","datavalue":{"value":"5558120","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1019024$9329E8F9-5EF0-48CD-82E8-3BE628A71FC3","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"25969ef3ed55d4d79dc66b72b9f8f40a00a019bf","datavalue":{"value":"interactive proving assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q1019024$8060497B-3DAF-4749-8DAB-414F596A15F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3e3ba7951b4903ad74bc8156ee379fa7f0472a6f","datavalue":{"value":"computer-aided verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1019024$0350E469-E43F-4957-9C3E-7DD2F2A67265","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"08339a711c129a2fe8b8478ada3bf5f872c2fcaf","datavalue":{"value":"teaching formal methods","type":"string"},"datatype":"string"},"type":"statement","id":"Q1019024$9E0FCD98-418C-4C8F-B05D-EE8C57226738","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"322cfa9d250a6a53032394dc0d9f662b03cdb062","datavalue":{"value":{"entity-type":"item","numeric-id":19193,"id":"Q19193"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1019024$F5FC5D84-E112-4E8B-B3A4-BD736BF4E30D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"cd543fd49199b1838ba332ea5e7b335fbe6c5a58","datavalue":{"value":{"entity-type":"item","numeric-id":19608,"id":"Q19608"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1019024$850E8BB4-9B7D-4515-BA8D-BD64D1812CC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1019024$35CA6B83-924C-494A-876B-070CF78CCD7A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1019024$E0B01B8A-A999-44C3-9F76-F8F1F14E6353","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"261ae6dfeffd96c9ea238e124055221c78337064","datavalue":{"value":{"entity-type":"item","numeric-id":13705,"id":"Q13705"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1019024$744B36CF-DE1B-4E24-9A0A-BF2013FFBEBE","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":"Q1019024$9A3F2BD4-6678-4F94-A71A-A52F1B5C8101","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5e89a906b0f036556895518d3377262109dfce20","datavalue":{"value":"https://doi.org/10.1007/s00165-008-0069-4","type":"string"},"datatype":"url"},"type":"statement","id":"Q1019024$87C97A6F-D17A-448B-BFD2-EAF577F86D43","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e0f25d360da5e42e592ad8c0e7b8459bd6ed3a70","datavalue":{"value":"W2007452988","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1019024$AC945426-4B36-4CE4-A447-377859700940","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba410b9e12f5248fb1a467353448eb8e12f87fa2","datavalue":{"value":{"entity-type":"item","numeric-id":3559759,"id":"Q3559759"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1019024$8BAC56DB-32C0-4009-8E24-675739034CC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9be67f799ffc5b3fd133657f657d0609a463820d","datavalue":{"value":{"entity-type":"item","numeric-id":5312942,"id":"Q5312942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1019024$6E3231AE-D1B9-4DFC-BBAD-E667550FC0DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c7e013849775846918727fac3e7e6455bd448813","datavalue":{"value":{"entity-type":"item","numeric-id":865646,"id":"Q865646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1019024$3A1C4418-9264-45C7-9396-74407D501B00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8bf1eb0085816c68ff7078182501fe6b0337105","datavalue":{"value":{"entity-type":"item","numeric-id":3743300,"id":"Q3743300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1019024$1900E953-7DAF-436B-90B2-71EBF53BB92F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"323dbd6fd6973b3663055cf97da83be885dd9ec7","datavalue":{"value":{"entity-type":"item","numeric-id":5569944,"id":"Q5569944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1019024$B88E10E6-5019-47B9-B9D9-2DD524A05A26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"672be30d9c0fd1bb08a1fc6131d1506ec245277a","datavalue":{"value":{"entity-type":"item","numeric-id":4830107,"id":"Q4830107"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1019024$A90EBA13-A04F-4C2D-9DE8-CDB191F49FE1","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":"Q1019024$B19FED6A-0FAF-4337-8559-65C481C22B88","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"22aaee8f908f3af7d88f218cda1c47300b68d77d","datavalue":{"value":"10.1007/S00165-008-0069-4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1019024$659E7FED-10FC-4054-9B4F-81505B8DC0B8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"757e822784b4bdc641199b06bea0bf174e7498e6","datavalue":{"value":{"entity-type":"item","numeric-id":832103,"id":"Q832103"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d4a9b0af1e7e577a30821ce01bd23004f2bbda3f","datavalue":{"value":{"amount":"+0.7654790282249451","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":"Q1019024$746C2261-4C2B-4525-B021-33D6C5FF0CF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"597f4e57288cc1698bfd2fe5e4fa5bcb6ae4d4fc","datavalue":{"value":{"entity-type":"item","numeric-id":3559759,"id":"Q3559759"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"18380be69b110aa1d69348bdc81791d3be70acb0","datavalue":{"value":{"amount":"+0.7353116869926453","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":"Q1019024$9D2202A9-025B-46F9-8EFA-C9CEECA4B81F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d66339c795d505f780406e18e20e0f95f8bd017d","datavalue":{"value":{"entity-type":"item","numeric-id":2729065,"id":"Q2729065"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ec09701fe9f4473ebae398db7eedc1e265d024c2","datavalue":{"value":{"amount":"+0.7343472838401794","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":"Q1019024$8BFBA956-E582-44E4-8EE2-1F78E71F4343","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"56d606835397ced889225aa24646e03238343394","datavalue":{"value":{"entity-type":"item","numeric-id":3000661,"id":"Q3000661"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fe727b3147ef413fb71443c866cea139632a408e","datavalue":{"value":{"amount":"+0.7327218651771545","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":"Q1019024$0FDBFABC-B43C-43F5-8857-5B69C7717DCF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4ab8385e60b2d92832b7d9f00cb7ee75d33b687c","datavalue":{"value":{"entity-type":"item","numeric-id":4499291,"id":"Q4499291"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c2494823377fdd6c21c5630e0405e369e0eeaf3f","datavalue":{"value":{"amount":"+0.7271575331687927","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":"Q1019024$E5A8C1CE-2741-419B-8075-CFD87D9B809C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The RISC ProofNavigator: a proving assistant for program verification in the classroom","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_RISC_ProofNavigator:_a_proving_assistant_for_program_verification_in_the_classroom"}}}}}