{"entities":{"Q1273080":{"pageid":1283830,"ns":120,"title":"Item:Q1273080","lastrevid":68348037,"modified":"2026-04-12T23:06:20Z","type":"item","id":"Q1273080","labels":{"en":{"language":"en","value":"Program construction by verifying specification"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1228843"}},"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":"Q1273080$65F0C067-4DCB-4D71-B68A-7150E9D55041","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8efa0e0de48f2bed1963e5d919a0a94a5ffce70c","datavalue":{"value":{"text":"Program construction by verifying specification","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1273080$E25AB001-C275-4D3C-883C-76C2F36E1F11","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"13e38a0c993b6708046b7a6fd85e448dea6a10b1","datavalue":{"value":"0911.68021","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1273080$3B53A2B3-6C0D-4AD8-ACF9-0B3AB17C3448","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9d6e996813e5c47e7f4845991824363e5a606998","datavalue":{"value":"10.1007/BF02946503","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1273080$DDF99855-9650-4841-A92D-3BC4F4DE6519","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a5308a2836a3891ed944cb1a7a372bd80b9713b1","datavalue":{"value":{"entity-type":"item","numeric-id":318846,"id":"Q318846"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1273080$75D624CE-291C-4873-A41E-89E90F5A4E5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f7fe40479c00e040397f1228a9a1c528b1efe34f","datavalue":{"value":{"entity-type":"item","numeric-id":1406565,"id":"Q1406565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1273080$DA1B6B0B-E547-4A92-9BF8-E30925356558","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"4c3c57bd2a24956e0520aebbb172d094d92623f1","datavalue":{"value":{"entity-type":"item","numeric-id":182337,"id":"Q182337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1273080$8E06FB01-9167-44DF-B504-668753E67444","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2ca81668723b17b38fcd31dd2e967490600b6d1d","datavalue":{"value":{"time":"+1999-03-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1273080$2349882D-A50E-46D6-88A5-5BA627014AE6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8e3f40e3cc87753c4e0b7d7ce4bdc00805f626f","datavalue":{"value":"68N01","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1273080$91264611-39AD-4112-91A8-2C4635478B6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1273080$CDBE2ECC-9A6C-4F42-BF11-6D91B015B1A6","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"668a8687db7bec9874ffc0718780ead88d71900b","datavalue":{"value":"1228843","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1273080$857D7B32-FD21-4AB6-86B0-CF00DC7DFD6A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1e7d5a44cae78ff970f139289090b69f93781a42","datavalue":{"value":"Gamma language","type":"string"},"datatype":"string"},"type":"statement","id":"Q1273080$CD46C396-2096-49C5-B86C-162A8F4DCC0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f4cee31b109bfd0275ef9410b844f3bfc242cf31","datavalue":{"value":"first-order predicate logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1273080$4DE098F5-A8CB-42B7-97FC-BFAB612CD3E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"794006a95fd0a6987d48feca647d9257f961094a","datavalue":{"value":"semantic verification program","type":"string"},"datatype":"string"},"type":"statement","id":"Q1273080$4784103E-CA2C-4F47-B3C6-1BAEE1A63DAB","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"17cfe6afe68a54e81dc559ef2cd5a702765207b0","datavalue":{"value":{"entity-type":"item","numeric-id":25375,"id":"Q25375"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1273080$8EFAACF9-F051-4696-BB1F-D41D4D707733","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":"Q1273080$2BB67612-AFDA-4512-8D96-6D8298F99899","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"10ac9eac2a61578c2e8597ae0765497583cb7b85","datavalue":{"value":{"entity-type":"item","numeric-id":1823657,"id":"Q1823657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1273080$C7F5EF98-C1C8-44F9-A106-35B3D5B2BADA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3619d6a42a8296cf679b0b994f59c7d8fc00a60d","datavalue":{"value":{"entity-type":"item","numeric-id":1100879,"id":"Q1100879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1273080$7245B1BB-87C9-40FE-96BB-4D157287B9B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a6659e15c68598875fe893d50af295f9d2c1d304","datavalue":{"value":{"entity-type":"item","numeric-id":918221,"id":"Q918221"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1273080$C5C93A87-E7A3-478C-9154-2EFDD28846E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6d0342acc4b6d3d5710fb00275aba55a9d8ae424","datavalue":{"value":{"entity-type":"item","numeric-id":751838,"id":"Q751838"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1273080$78E2C62A-1E2C-45BC-A4CC-E0E63C4D1D23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"288101ca16719641b6d826c50f535fd8613a7b93","datavalue":{"value":{"entity-type":"item","numeric-id":1822927,"id":"Q1822927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1273080$D04B90CB-2FB1-4010-B306-94DD5032A9AC","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":"Q1273080$4437651F-FCB4-4593-BB8A-F022B98589F9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3b40bee1b309e302d67a4b5de1d4684375d31f21","datavalue":{"value":"https://doi.org/10.1007/bf02946503","type":"string"},"datatype":"url"},"type":"statement","id":"Q1273080$2E3AF6BD-D590-40E5-93E6-7900B91EA1A7","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"8a929c9c44c453362ae47ea7ac6fd4d53a65bbf4","datavalue":{"value":"W2021599033","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1273080$A4B4FB68-8ADA-4876-8913-DC1CD976FBE8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"11408dd6eb63e6af3770ee4f45371eb4682c5354","datavalue":{"value":{"entity-type":"item","numeric-id":3152931,"id":"Q3152931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"074d8def0b25efc7d69d67d33823f0906e77f4dc","datavalue":{"value":{"amount":"+0.7593734264373779","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":"Q1273080$9585A9B9-6443-4FDF-9746-30C84D5B9353","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cfd98f2abb2e6d695d1a88d96506627a8bad2bbf","datavalue":{"value":{"entity-type":"item","numeric-id":3575262,"id":"Q3575262"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a9653f035dad2d426ab958e24ff0af5cb43f863c","datavalue":{"value":{"amount":"+0.7424853444099426","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":"Q1273080$8301E2AB-7616-4278-B51F-1BCB97B41954","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bf46f319d63f9e0789f735f4c58c45d4094b2ea7","datavalue":{"value":{"entity-type":"item","numeric-id":3780492,"id":"Q3780492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f3fad2c8b4d0785121f913c19325e042f9e8113a","datavalue":{"value":{"amount":"+0.7405389547348022","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":"Q1273080$8270BF49-EA27-4B89-A44B-EF5A7BCE3695","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ba7621710cde78fddbc5ccfe98349da8b74f85a7","datavalue":{"value":{"entity-type":"item","numeric-id":4341024,"id":"Q4341024"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ef05ec4f02a83bc97c7d7550af3494a813936a0e","datavalue":{"value":{"amount":"+0.7361235618591309","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":"Q1273080$893CC61B-A293-4200-A4E9-DDF961C995C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"714e15e5a2ba4fff06e9121fed38d3236869a4fd","datavalue":{"value":{"entity-type":"item","numeric-id":1267035,"id":"Q1267035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e76d8363a5921b8a69a3b60935bf6e9ab7d8c0c0","datavalue":{"value":{"amount":"+0.735801100730896","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":"Q1273080$3F0270B8-4205-4F08-AC4A-EF035D1F1E3A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Program construction by verifying specification","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Program_construction_by_verifying_specification"}}}}}