{"entities":{"Q916409":{"pageid":918257,"ns":120,"title":"Item:Q916409","lastrevid":65325735,"modified":"2026-04-12T01:49:33Z","type":"item","id":"Q916409","labels":{"en":{"language":"en","value":"Refinement concepts formalised in higher order logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4153902"}},"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":"Q916409$B2D29550-012D-45B8-95B1-E0159092D0B2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7e493e90b251443945a452d0f32ad6fd4202455e","datavalue":{"value":{"text":"Refinement concepts formalised in higher order logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q916409$5615AF4B-FA70-4B5E-A0F2-9949F5F4D3ED","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c560b436e50d958d5b992c1687003145760474f0","datavalue":{"value":"0703.68074","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q916409$31A1BC43-49BA-43EA-BD2D-ECC75BD8D362","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"056020d1c3482cd607ef8d9aa72ebb3e744d8b40","datavalue":{"value":"10.1007/BF01888227","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q916409$C2DEF4AD-A980-47E0-A15B-7ED484091EEC","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3d56612cb84f7069100c4cabafc4cc7f11973342","datavalue":{"value":{"entity-type":"item","numeric-id":914554,"id":"Q914554"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q916409$19A8FCCB-B51A-42E5-AE6B-7E18B0538472","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":"Q916409$D0E99DCF-4096-4B40-9D68-6F139068AF76","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"70d2fbf8bcd48a5ca1ac752985098b379d0dbb65","datavalue":{"value":{"time":"+1990-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q916409$D2F4C08A-4596-47C8-8EE1-E8C17CB1CEB7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q916409$72AF2FE3-27C6-4242-B8CD-33CAA31F3564","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q916409$BA6ABB34-1406-4F63-8D5F-74C798AD97AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q916409$0FA0CFE3-EA69-4D22-AA27-8481713F77C5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9565c6a975e0bab3f441936364851b3a7d03e823","datavalue":{"value":"4153902","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q916409$01030E64-6C8F-4D05-91F3-F82E575F802B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a2db40c62fbba481c23c52e595e1d3bd4320088e","datavalue":{"value":"mechanical theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q916409$43288F4A-BDD9-4FF0-B0F9-F4E8792CA2C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8199d3c167bb7194c1f4325dd8abc9ea993e9d4d","datavalue":{"value":"program development","type":"string"},"datatype":"string"},"type":"statement","id":"Q916409$335B846D-9481-4DA2-8E3D-E64C924EC1D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"40e17a7cb8710771acd5402f91cff6ae2c7d64aa","datavalue":{"value":"refinement calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q916409$8ED92035-02F0-4A13-90DB-4E3341079939","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"26325b97ca9f91dadc7bc17af7514ea7907cb4fa","datavalue":{"value":"weakest precondition","type":"string"},"datatype":"string"},"type":"statement","id":"Q916409$FF4F2F23-5DBD-49E4-85AE-7B9DB15CC5B9","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":"Q916409$B96BADB1-3C9E-4BE3-858B-B8049EDDBE70","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":"Q916409$5275A267-2B74-472E-AEBE-6B1FA8924D83","rank":"normal"}],"P223":[{"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":"Q916409$1EFFD38A-CB33-4562-A7B1-B314504E69F8","rank":"normal"},{"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":"Q916409$CE332942-464B-47BF-9A5C-051F2028A687","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"94223dafefd21030be656dcd94f94b2f0ec420de","datavalue":{"value":{"entity-type":"item","numeric-id":918204,"id":"Q918204"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q916409$93123CED-2993-43CE-BEB6-E08D7B67E8EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86f96f1b5184988ef14c3a8dd82b1d2786ba8272","datavalue":{"value":{"entity-type":"item","numeric-id":913495,"id":"Q913495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q916409$BC09724C-E809-4A01-932A-42DFBE434C2F","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":"Q916409$99F6437B-104C-4832-92F2-DC885BD1FAE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a7493c00c260f207a238f41e9e5a3d8b8ed81bd7","datavalue":{"value":{"entity-type":"item","numeric-id":1075045,"id":"Q1075045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q916409$9A229E52-B295-461F-91F5-51EA1DEA823B","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":"Q916409$DBCC788F-45D2-4854-B3FA-C8EC95FFFBD5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e47b8c90d45ee285590b1a168a8503851fe5b134","datavalue":{"value":{"entity-type":"item","numeric-id":3925859,"id":"Q3925859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q916409$9FA19826-4013-4810-A6D6-8E806B654A81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cc8abb92210655a5bd4143cbbadd6eadb52d635","datavalue":{"value":{"entity-type":"item","numeric-id":1801222,"id":"Q1801222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q916409$C70BDAC2-6087-45B9-958F-E36818E8F59A","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":"Q916409$326CCFCA-1FA5-46F0-B6E6-21B45CED2D2D","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":"Q916409$17CD40A9-7A57-4183-88B0-5933354E296A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0be2d7a498e1fa1a8eec9f77d2e3dbc81e945234","datavalue":{"value":{"entity-type":"item","numeric-id":3906397,"id":"Q3906397"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q916409$BB37855E-0479-4970-BEDA-5EBA45698C2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e320d5ab20d9378e83c08a862b63bf2725892d4a","datavalue":{"value":{"entity-type":"item","numeric-id":2653567,"id":"Q2653567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q916409$9334D968-0A7A-412D-A985-A55024700E99","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"14dec9a89d8068fb1e5713e5cc72d0b606ce6088","datavalue":{"value":{"entity-type":"item","numeric-id":1309250,"id":"Q1309250"},"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":"Q916409$5F163083-68AC-445C-AE38-7E5F59AE5731","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":"06c5d5193a6b321b52b5b606dd969bf8e6b99b82","datavalue":{"value":{"amount":"+0.7814949750900269","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":"Q916409$4418C966-D755-4806-BAD5-0FD342DAC60A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"524d090d085cff50384ab46fc0b59b96caa6d641","datavalue":{"value":{"entity-type":"item","numeric-id":3079921,"id":"Q3079921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9886a838f43039955e969abfc8269f391b0ecff6","datavalue":{"value":{"amount":"+0.7750941514968872","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":"Q916409$35280770-F41A-44FC-86FE-7C12EF0BB6F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"75ee5105ce557480702c4228fc94eceba0497db4","datavalue":{"value":{"entity-type":"item","numeric-id":1111362,"id":"Q1111362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"900f850b32895844aa762b8324b932bf1b986fb3","datavalue":{"value":{"amount":"+0.7693625092506409","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":"Q916409$4AEC0D42-14D9-4006-9009-96A5F0750280","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8fd5c2832aabbf4b304824c9b3020a0ed9253b4e","datavalue":{"value":{"entity-type":"item","numeric-id":4823141,"id":"Q4823141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9bfded777109c61d146b5597ce1f90d4e6967d80","datavalue":{"value":{"amount":"+0.7517794370651245","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":"Q916409$518565C2-7AEE-4310-9D71-97CF98B9FBB7","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Refinement concepts formalised in higher order logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Refinement_concepts_formalised_in_higher_order_logic"}}}}}