{"entities":{"Q1309250":{"pageid":1320000,"ns":120,"title":"Item:Q1309250","lastrevid":67128123,"modified":"2026-04-12T15:28:51Z","type":"item","id":"Q1309250","labels":{"en":{"language":"en","value":"Mechanizing some advanced refinement concepts"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 469139"}},"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":"Q1309250$ED859C0A-20C7-4963-9099-834308953181","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6e8f73cc8f8ba2cf862c079bfa014f7ddd4d139b","datavalue":{"value":{"text":"Mechanizing some advanced refinement concepts","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1309250$6D11C97C-5C1E-460B-954B-13561E6576AA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4c9078d6b916eed4418dccfc60bfb7a720ba4970","datavalue":{"value":"0785.68063","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1309250$8835A535-1B31-45DC-8976-4A9D4E979A05","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"48fa03198378d78e34f8c07d890826560b271445","datavalue":{"value":"10.1007/BF01383984","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1309250$9EBDA8BA-4089-4D65-92AD-6E8C316ACE1E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a88a8725eba02785396684fc7e2a164a503a6220","datavalue":{"value":{"entity-type":"item","numeric-id":1309247,"id":"Q1309247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309250$9D0FCBF8-E02D-4130-AD4B-4104A684544E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"667c2fac247a417afbe52ef306e5ab86dd0d7cd8","datavalue":{"value":{"entity-type":"item","numeric-id":1309248,"id":"Q1309248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309250$A0FC3511-B2CC-4620-8B26-18CF8B6EC164","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"72573f50435147b1a906bcad32e0521fcefe619e","datavalue":{"value":{"entity-type":"item","numeric-id":1309249,"id":"Q1309249"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309250$4E26CEA1-49AC-4FD5-A110-CE363751AD4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"48d865be380a2417118adfe1d5342583c2c12e0b","datavalue":{"value":{"entity-type":"item","numeric-id":204600,"id":"Q204600"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309250$A1BFDE11-09A1-495C-BD7A-9961A7E99403","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"70551fcc6e89042fc26ae9242a005533b44a2d7a","datavalue":{"value":{"entity-type":"item","numeric-id":169908,"id":"Q169908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309250$C0F9BC43-1B56-4827-B6AD-63E257575AF9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c23015971af1177ae2bf4a3e2bb7dae4f44d2a62","datavalue":{"value":{"time":"+1994-04-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1309250$08BAA178-8A96-4A89-B77C-5BA92ACE4AD1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1309250$CC9DCCD0-7895-4420-BCCB-B65007F9C8C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1309250$22A3C59B-87D4-47AE-8475-E115FCBFDB37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1309250$BC431F65-3CEF-4B9A-9823-7757F4EB298D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d91213212b773cb06f526c0aa4af3f8e325a4f4a","datavalue":{"value":"469139","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1309250$D8C1AC8F-D137-4EE0-A896-D9727BA22CEE","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1309250$52EE6E04-4EFC-42A1-AAD5-B4D44D46B1C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1aee419b13f29f23efa882f3ada4c59260850cf2","datavalue":{"value":"semantics of programming languages","type":"string"},"datatype":"string"},"type":"statement","id":"Q1309250$556B7310-1F31-4828-BA6D-0CE22690F012","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7c2a9a0ee15dbb4bfd89047300f0dab1f2cb4127","datavalue":{"value":"HOL theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q1309250$2752B1E3-F366-4E50-93C4-45728316665E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9e04a9b6f29796c4d02ff2b937276cb784681560","datavalue":{"value":"program refinement","type":"string"},"datatype":"string"},"type":"statement","id":"Q1309250$CE7DC13E-CFCA-4120-A9BE-2022378943CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4f1256c8b0070c66f4228355c755698c708a9c34","datavalue":{"value":"program transformations","type":"string"},"datatype":"string"},"type":"statement","id":"Q1309250$7B55BD29-6040-42B5-8A8D-4315942AB3E7","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309250$DB519784-18CE-4743-BE69-21E90C371783","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":"Q1309250$828C0AFF-36D2-4B05-AFB8-9EF9811B35A8","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d99c5a0e13ee889036714bc5394088e5f34dd18","datavalue":{"value":{"entity-type":"item","numeric-id":1111362,"id":"Q1111362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309250$6C962CFC-9E2A-444B-89B3-EAB0B18C47A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e8576dc8df0d7857399ab718724b601efc6d9d7d","datavalue":{"value":{"entity-type":"item","numeric-id":3996918,"id":"Q3996918"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309250$87B93340-165E-4E6D-8B80-755FBC0BE85E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"67b8a6374b4fc895d89506f759c76e54380f8254","datavalue":{"value":{"entity-type":"item","numeric-id":4144755,"id":"Q4144755"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309250$68022616-BDE7-4AD8-9042-766C33E17DE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"145ba4ed8ff284bc41a418ac8911941d54ea5802","datavalue":{"value":{"entity-type":"item","numeric-id":1177155,"id":"Q1177155"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309250$29219560-D1C6-4F20-9D00-BAD1DC6D3590","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cc9dcf97f1324642e65a88c0357ad0c7fec47b09","datavalue":{"value":{"entity-type":"item","numeric-id":1113664,"id":"Q1113664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309250$6020D877-518E-4900-8140-645D226F7EE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"83e646822c7e8f7e68867ade26f59c8b15d8260c","datavalue":{"value":{"entity-type":"item","numeric-id":3707340,"id":"Q3707340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309250$55D52967-CA30-4B96-B036-C5C8CFA6CEC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"090e4b104dd3f76f7e7cbd674cb41b2227a87ff1","datavalue":{"value":{"entity-type":"item","numeric-id":4692502,"id":"Q4692502"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309250$48EC30D6-7C14-4C39-9D3B-4AA7C6064D47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a391224903bcc05aa0957fd51168c79b7b870f96","datavalue":{"value":{"entity-type":"item","numeric-id":4028640,"id":"Q4028640"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309250$15E85899-EBA7-4E97-A89C-CC32F41A113B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c3877a1f64445e2be38ffa92491ece3830dcf80","datavalue":{"value":{"entity-type":"item","numeric-id":916409,"id":"Q916409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309250$0E02250B-34ED-444B-8862-EC400A3EC725","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ca7e027091589776f78a6d7ad8457e805c17b28","datavalue":{"value":{"entity-type":"item","numeric-id":5777498,"id":"Q5777498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309250$D3D94C35-5570-43E3-B977-284671BE40A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bd265bdbcf41f2b9982b655d7aaf44e4072217fa","datavalue":{"value":{"entity-type":"item","numeric-id":4692630,"id":"Q4692630"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309250$D0EC5DB4-C0E1-4FD0-81ED-686B432A5925","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7469a14c6b3d5214a08da9b6d9960375ad8bda98","datavalue":{"value":{"entity-type":"item","numeric-id":3898009,"id":"Q3898009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309250$1D55D1B2-0795-4E58-AE6E-5317FAC2763D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db45f234f354c516e6967660fb11814401792350","datavalue":{"value":{"entity-type":"item","numeric-id":578892,"id":"Q578892"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309250$D71E9689-0D4C-4017-832D-A59711F76D60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad0b116a99357b3d672b8fba8948de48e57254ee","datavalue":{"value":{"entity-type":"item","numeric-id":1199826,"id":"Q1199826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309250$72D1435E-910F-4D5C-871E-882A461315CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d643c9519505ce70f954afc2ea3c543e896e9fb9","datavalue":{"value":{"entity-type":"item","numeric-id":578901,"id":"Q578901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1309250$65AAF50B-EE60-46D1-B9D4-04B1617948B9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b381385eb2a7e6b63d2ca46318098498c93c4161","datavalue":{"value":"https://doi.org/10.1007/bf01383984","type":"string"},"datatype":"url"},"type":"statement","id":"Q1309250$B1ACEF24-E24C-4BDF-A7E3-71D0E32C8398","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"1b73fd42aa5b4e3cca5031c5fa107a9817f79497","datavalue":{"value":"W3021087793","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1309250$079CF3DC-CB81-4E59-9ABC-DF46DB5AE539","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dc34f59ed8e9f7b8abc3b304054cb60be3fbd4eb","datavalue":{"value":{"entity-type":"item","numeric-id":916409,"id":"Q916409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7dc24be114c049bb080183c82608d375c9bbf1c2","datavalue":{"value":{"amount":"+0.8221972584724426","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":"Q1309250$D229F383-03BA-4FF9-8025-BACA31E14FE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"012c23954d4f438873067eae5f473ad4270bcc00","datavalue":{"value":{"entity-type":"item","numeric-id":4370252,"id":"Q4370252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e61115229af36ced5cdc2ebc32362aa29d508d6c","datavalue":{"value":{"amount":"+0.8001423478126526","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":"Q1309250$9E02962C-85C1-4892-A709-8CB617A24051","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"070be8014f9fa1d5144a124153513a7ad9916e87","datavalue":{"value":{"entity-type":"item","numeric-id":4250665,"id":"Q4250665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"583424f8b01dec8eb21c7c4d62c5b076f83ae65d","datavalue":{"value":{"amount":"+0.7791590094566345","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":"Q1309250$4BEA538A-982B-4A6D-9974-2ABD48D3D5B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"46d2f1aea5bca1e9ea33d09f2dc7fd2cfef54aa7","datavalue":{"value":{"entity-type":"item","numeric-id":4790664,"id":"Q4790664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5559a19a3774ca76a4d6840abd831b7a3d2aa263","datavalue":{"value":{"amount":"+0.7753356099128723","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":"Q1309250$07DABD84-BAD0-4C7F-959A-43240410F38E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"551c3030ce794fadfa9659c442c44464cdaf83f8","datavalue":{"value":{"entity-type":"item","numeric-id":1272759,"id":"Q1272759"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"84b9fb27ac4368d5d6f969f14a3fdd68354714e6","datavalue":{"value":{"amount":"+0.7669029235839844","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":"Q1309250$07A82ACF-9280-49EF-AD1A-4CECB2430CB3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Mechanizing some advanced refinement concepts","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Mechanizing_some_advanced_refinement_concepts"}}}}}