{"entities":{"Q3431400":{"pageid":3442103,"ns":120,"title":"Item:Q3431400","lastrevid":50068216,"modified":"2026-01-12T21:01:27Z","type":"item","id":"Q3431400","labels":{"en":{"language":"en","value":"Structured formal development in Isabelle"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5141408"}},"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":"Q3431400$C0077321-8441-424E-A20A-1737F0DB5221","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5cf8d14fde8cc3bfdc5b4ad84ae22e728b6586ec","datavalue":{"value":"1114.68063","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3431400$6F56D0E6-5ABC-4F37-B667-E7A6399A8309","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6884dcd553d8669c30774eb71f232565b4c5e680","datavalue":{"value":{"entity-type":"item","numeric-id":3431399,"id":"Q3431399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3431400$0A75C95E-48E1-4309-B897-00A7B26390FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"766a7b4a0daa5b8547ebae773097f31bce780235","datavalue":{"value":{"entity-type":"item","numeric-id":444464,"id":"Q444464"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3431400$5E2E3ECF-70D4-4503-B2B6-08B2BAF83158","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ce00bf932e8d4142816bb1d3b66ef3457d10b848","datavalue":{"value":{"entity-type":"item","numeric-id":626932,"id":"Q626932"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3431400$6F713935-CD79-4650-9C14-E7501F007853","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7130f17776024677519259de1aa3e6f876677651","datavalue":{"value":{"time":"+2007-04-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":"Q3431400$4B04F0FE-0683-4B45-A289-F8704A0B2A50","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3431400$A282CC86-567F-4C39-B67B-1BEC9B9AD25E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3431400$F30E23C1-1EE3-4ADD-9070-742347D4D323","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3431400$E48389E9-909D-419D-A6F6-3245DC07A632","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3fe48bb2530751f70feb823e22bcf7a5e8b5be8e","datavalue":{"value":"5141408","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3431400$E4295FAD-A0BF-4B40-8641-933E262CE2AD","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8199d3c167bb7194c1f4325dd8abc9ea993e9d4d","datavalue":{"value":"program development","type":"string"},"datatype":"string"},"type":"statement","id":"Q3431400$A20D195E-8580-4842-9FCB-12B454DED6CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b36661f0a3390102be2be05796702400601b738","datavalue":{"value":"theorem provers","type":"string"},"datatype":"string"},"type":"statement","id":"Q3431400$B9AF98CF-26AD-4AA6-8F0A-FA79066EEC7D","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bcaf3b20cd7fd897f2f47a708bad9d4f554cb6fa","datavalue":{"value":{"entity-type":"item","numeric-id":14553,"id":"Q14553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3431400$E8252433-A54F-408F-85F3-9DF03ED12B62","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":"Q3431400$A0C0BAC9-19FD-48EE-8C2E-75A34D53500E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"99e87bd3628666ae4ab034c6ef4dffb80dd2f85a","datavalue":{"value":{"entity-type":"item","numeric-id":13712,"id":"Q13712"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3431400$6BB73692-BA41-46CB-BB69-D46BA69782C0","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":"Q3431400$2C440E93-F5F5-4E7A-B849-81023323C877","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"441897fe7904c9e44fbfc08e8a7a55eaf5c3e772","datavalue":{"value":{"entity-type":"item","numeric-id":5392587,"id":"Q5392587"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b37e60f8a74aaefb1f53092d6383fd56757fd3e4","datavalue":{"value":{"amount":"+0.8431766629219055","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":"Q3431400$CB456837-16A3-4F08-99A5-784430E996E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6355fdcd09db84aad056c40c86e8fba6296f0644","datavalue":{"value":{"entity-type":"item","numeric-id":3582695,"id":"Q3582695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"25f0fb258d283f1d4066d2fa2760b3ae2f922942","datavalue":{"value":{"amount":"+0.83269202709198","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":"Q3431400$5B32FA0C-AFC1-4167-AB2D-BB5865C85CC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ef914c5d16ae991870856bd539a5283395a477b7","datavalue":{"value":{"entity-type":"item","numeric-id":3543647,"id":"Q3543647"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d5fdeef1a68b983f9d14b14075c4ad7866ee20a5","datavalue":{"value":{"amount":"+0.7713761329650879","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":"Q3431400$CAEB0786-856B-4A59-B109-49CE610F7FDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"619d07d39ad50d8b9a4d0bfcd8121f291b2fc77d","datavalue":{"value":{"entity-type":"item","numeric-id":4364537,"id":"Q4364537"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5685a426cdae09a62716a699000d32e2540f6479","datavalue":{"value":{"amount":"+0.7710890173912048","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":"Q3431400$8FF91A0B-5AA2-4D5E-9710-A2CFA3A17886","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"027e66e493294de396e3f06701b232a3660c5eaa","datavalue":{"value":{"entity-type":"item","numeric-id":1823013,"id":"Q1823013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a38b1812cd70c17aaa90f12bfcb3d9a637384edb","datavalue":{"value":{"amount":"+0.7506173849105835","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":"Q3431400$569EBFC2-4384-4032-88F0-4405C72F4BF5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3431400","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3431400"}}}}}