{"entities":{"Q4624465":{"pageid":6654048,"ns":120,"title":"Item:Q4624465","lastrevid":53367275,"modified":"2026-01-24T20:08:45Z","type":"item","id":"Q4624465","labels":{"en":{"language":"en","value":"The formal derivation of algorithm and automatic verification based on Isabelle"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7028683"}},"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":"Q4624465$B3D088BB-05A3-4033-A32B-4D5B6C5673F3","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"111d469b03bd25a317662d9b1bdbe18a74ac1408","datavalue":{"value":"1424.68041","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4624465$0DB6836E-38C1-4F0D-9775-0AE989D21CE8","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"634888f5b5cc60035599e775ea60c4ae66dde83b","datavalue":{"value":{"entity-type":"item","numeric-id":4624464,"id":"Q4624464"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4624465$E8453429-7F48-4367-A670-B1C164C0ABCA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1444e03740a889f03677a78c93b0e852b4c40e4c","datavalue":{"value":{"entity-type":"item","numeric-id":3017146,"id":"Q3017146"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4624465$1CFE3E5B-0F04-4F15-A2F9-32E44E2C4FFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"48a887536c7092529db5959221036a8ea5ba17b4","datavalue":{"value":{"entity-type":"item","numeric-id":839756,"id":"Q839756"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4624465$6147DA3F-4434-4740-AA73-FE97173FE573","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"de6231e2c15042f8d09f82d34b78d1fbec842408","datavalue":{"value":{"time":"+2019-02-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4624465$91028238-312D-43F1-82BB-8589FF548264","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4624465$04520771-C98E-478D-8D4E-44B4C77F3F21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4624465$A753CC6B-DF7A-4303-959C-01EBBBF2FCB4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1eb4bac400ad32529512334599144365655a8a2b","datavalue":{"value":"7028683","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4624465$62578787-1C61-4111-9E80-9F3BA9B3FC10","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f02f4db7bd17ba3fbae1be6bcee13dc9e5aa86bc","datavalue":{"value":"formal methods","type":"string"},"datatype":"string"},"type":"statement","id":"Q4624465$70F5EDAE-8C6D-4A55-A705-F66D0988073C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bab2ce6b29cefdf4b2cde9a3d0f1cb1bdf57d64a","datavalue":{"value":"Isabelle theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q4624465$80F39691-F432-45DA-A988-923F472B62C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c20b4fa4782bc26ad106d3b73d2e44447725459e","datavalue":{"value":"automatic verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q4624465$C5742403-6D1F-4B4E-B66E-D8D2B9F0F75E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"96c68a7f0960a495de8c26ecfb01174e6ba9f189","datavalue":{"value":"formal derivation","type":"string"},"datatype":"string"},"type":"statement","id":"Q4624465$5D76F177-9025-4DC5-973B-31D158B7E78F","rank":"normal"}],"P1463":[{"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":"Q4624465$BA0BBF90-E7D5-4C79-87F2-4C2177E8A887","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":"Q4624465$5D96ABF9-54E9-4DB6-8C63-24ADAD066F42","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"94da4657187bd7f9a776c69b8705d80b4714946d","datavalue":{"value":"10.16357/J.CNKI.ISSN1000-5862.2018.04.10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4624465$7DC252A9-1843-4A9A-A5D2-4133FE53633E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"92c8794b5870b1144c6b99b340ca9276a2b2d395","datavalue":{"value":{"entity-type":"item","numeric-id":5690664,"id":"Q5690664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f437b457319d326f004bac1d97422371647cc608","datavalue":{"value":{"amount":"+0.7198425531387329","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":"Q4624465$CD2D471C-E913-46FB-8D82-31F805647FAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0294f772afc45e1d2472e820f88e87f978718519","datavalue":{"value":{"entity-type":"item","numeric-id":5153485,"id":"Q5153485"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"73b4450d3340e42dc85ae5a14b52c809eb099b72","datavalue":{"value":{"amount":"+0.6885286569595337","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":"Q4624465$38C85045-4F62-4AA8-9649-43F2D932DFB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"13e649264ee8c5f77323097969c0d9813410c2c8","datavalue":{"value":{"entity-type":"item","numeric-id":2754046,"id":"Q2754046"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5491b60478af16bad769cbfb4eb2b21d465b6c1b","datavalue":{"value":{"amount":"+0.6877756118774414","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":"Q4624465$BB18AD6C-A2D7-490F-879F-886B29FFD4BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"afbd5bc9f9db4a8c8f5d78463047c2c327809d9c","datavalue":{"value":{"entity-type":"item","numeric-id":736840,"id":"Q736840"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"19d8c98a03661fdd3adb1ce6da04ab857a371a8c","datavalue":{"value":{"amount":"+0.6867701411247253","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":"Q4624465$0F05A5D5-DA49-419B-8E4A-AA17896BBA89","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2a0e6b204aeb44da7655072b1a414c4dab2f8d94","datavalue":{"value":{"entity-type":"item","numeric-id":2018423,"id":"Q2018423"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0c2f28a9b9cb7e6139e36f4e1f1ea73ce5e79d11","datavalue":{"value":{"amount":"+0.674206554889679","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":"Q4624465$BA74DAE0-0380-4C5D-BA19-B2A110E7FA0F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4624465","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4624465"}}}}}