{"entities":{"Q1334901":{"pageid":1345640,"ns":120,"title":"Item:Q1334901","lastrevid":67432782,"modified":"2026-04-12T17:42:51Z","type":"item","id":"Q1334901","labels":{"en":{"language":"en","value":"Annotations in formal specifications and proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 644674"}},"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":"Q1334901$7E1AE89D-6D6F-4A09-90DD-D8A283C8A570","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"711dc0b6c23a9e66971b6dea46cf7531cc7e71b6","datavalue":{"value":{"text":"Annotations in formal specifications and proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1334901$124ADA28-A16A-4ED1-AEEC-C05F8CF6F831","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"648fa08f1d1dc9b15ec10b2a21f9e19664f2f5a7","datavalue":{"value":"0814.68088","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1334901$971B2A49-1CB6-4BC8-93AA-E7222D323214","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c051d895736adcbe066f84479bc9c6ae2af5d118","datavalue":{"value":"10.1007/BF01384236","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1334901$DDE95485-4549-4D94-A217-47F3BF96B878","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b000e276c0b3e58eed33c6f221b1bd5f0e740e83","datavalue":{"value":{"entity-type":"item","numeric-id":1334900,"id":"Q1334900"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1334901$1FC49644-E950-43FE-8F66-4FB1913BFA06","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":"Q1334901$DE8E2458-9902-4FDB-9DF4-BF62E6C919F7","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a07e8af38f76d1e005ebe63136b3f3c24a5ff2b8","datavalue":{"value":{"time":"+1994-09-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1334901$E91EE0D0-8C1B-4D4F-99E8-E180CD00AF3F","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"74af6d28f775a3d512470d968e836305696f3166","datavalue":{"value":"In order to exploit the connection between the formal and the informal aspects of modeling, the author proposes a system of annotations that can be used to incorporate semantic information concerning the domain being reasoned about into a formal proof environment. Annotations will serve as comments, labels, or proof directives. An implementation in the HOL proof system is presented.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1334901$4C808D6B-4CF1-465B-BB59-2B15A8E0803F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1334901$8B79E443-1FB3-4C70-B04A-F97FEDBE98E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1334901$BC7D2741-07BF-4992-A033-1DB18BE29AD9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9a6f02d967994d1cdb1d2f41dda8134bc4d685e2","datavalue":{"value":"644674","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1334901$426036E3-C8C9-44A8-B0A8-28269D095443","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"87994eb840961e5165378eb7f918102952689b42","datavalue":{"value":"formal specification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1334901$E42AC3A3-E3D5-4493-B301-3AA75BAEDAEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66824d9cf653f7dee3c76f98a8ea1aa06432fa7c","datavalue":{"value":"verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1334901$604CF9E2-84BB-4362-9B12-98087A74B980","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1334901$EEFE9FF9-5E86-48B7-921E-DA8B26E5489F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4d2ba1f3a9d37aa907198949c7415e4bc2ead980","datavalue":{"value":"modeling","type":"string"},"datatype":"string"},"type":"statement","id":"Q1334901$1A754D19-27E3-4C1C-AB97-05B0A92EA931","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"ce55c35a0130dff40a2e46fd6cbf84198a7e9797","datavalue":{"value":{"entity-type":"item","numeric-id":590016,"id":"Q590016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1334901$F487B491-67CD-4CD8-AEFF-6E5F93853028","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":"Q1334901$997937A1-8854-4E6B-8479-B1AA2D1F227B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e07b63a7544a6d7c83390f82ddae368b77e124c","datavalue":{"value":{"entity-type":"item","numeric-id":19570,"id":"Q19570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1334901$27AA6549-BB82-4DB9-8BBE-C15031C5A9C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1334901$234C373E-C1FE-48AE-B905-9A87427AE9E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"56183f18c1b7292025f517695163436751950f86","datavalue":{"value":{"entity-type":"item","numeric-id":22253,"id":"Q22253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1334901$29A967C4-6D92-4742-AD2F-39F06FE5A6F8","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":"Q1334901$CB45752A-B3CA-403F-9852-455E1C404B31","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"135784055f6c7bf88f771b4cd8c0d6f7e263567e","datavalue":{"value":{"entity-type":"item","numeric-id":3660892,"id":"Q3660892"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1334901$A80E4D65-B193-4D07-AB06-BF80885A9767","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0aad2711eb9c64a58dada485191047b8af29959d","datavalue":{"value":{"entity-type":"item","numeric-id":4040283,"id":"Q4040283"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1334901$B8B95CC8-5700-443E-B347-2CF9D313578C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6821d8bf92570a1265d30079b71046c8a303a664","datavalue":{"value":{"entity-type":"item","numeric-id":3327746,"id":"Q3327746"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1334901$FCA12BF8-8428-419A-ACE5-022CBA79F765","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7d504f8f758d30af6cf41a7818010f5320c73d6d","datavalue":{"value":{"entity-type":"item","numeric-id":4723263,"id":"Q4723263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1334901$FD5788E2-248B-40D6-81A0-F966C3C6FD73","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":"Q1334901$2185221D-3002-404A-9500-EABB346D75F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77498059d5dae7644cba7115ca2a5485478e2bf3","datavalue":{"value":{"entity-type":"item","numeric-id":3783490,"id":"Q3783490"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1334901$D7F12937-56C0-4AA5-92A6-531306DCA20B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f62ebef9379ad97d2bdc3c2e7f5717f221d056cb","datavalue":{"value":{"entity-type":"item","numeric-id":5514129,"id":"Q5514129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1334901$8183DEAB-6C7E-4F06-9150-9C8B74C8A9A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f857559f497d88c44e56392a1ad488904465dae7","datavalue":{"value":{"entity-type":"item","numeric-id":3959414,"id":"Q3959414"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1334901$DDA58E1C-6792-42BF-8073-B41D59340429","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a2c73ea523922ddf10917d5a60c3c9e9df84e94","datavalue":{"value":{"entity-type":"item","numeric-id":3995087,"id":"Q3995087"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1334901$30E97E38-1BE1-4708-888A-49D2E4C832CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3223a1602d7869d2d8c43ffe2b6fa9827ae1a730","datavalue":{"value":{"entity-type":"item","numeric-id":4139639,"id":"Q4139639"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1334901$44DAD552-4CD0-42A3-9C1D-F80B666DD994","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aecc0acebfcc7a68b04001a52def5cbc40c650b9","datavalue":{"value":{"entity-type":"item","numeric-id":1601866,"id":"Q1601866"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2f182666d85db62570057106e4179f51d10d1a61","datavalue":{"value":{"amount":"+0.7142040729522705","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":"Q1334901$AD483D2E-99C3-4207-91C5-B0D30034D9A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9d90471b5e767ee22364b8325141c0566ae0d24f","datavalue":{"value":{"entity-type":"item","numeric-id":4443407,"id":"Q4443407"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3d46fa7ff857a800ea315583bec3d03fec930b37","datavalue":{"value":{"amount":"+0.7025430202484131","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":"Q1334901$9448FC81-6F88-4AEF-B11B-4A201A000CFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bc268baf51e6f99f0ec7fc0e4bd70830f2cc4651","datavalue":{"value":{"entity-type":"item","numeric-id":5302560,"id":"Q5302560"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"27622d90d321acf1316d98bd97244848173343da","datavalue":{"value":{"amount":"+0.6995981931686401","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":"Q1334901$6F836AAF-AD21-4781-8520-A8185F5A74BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cc73622dd17a1093cfb9f852be76751bfdd17dc7","datavalue":{"value":{"entity-type":"item","numeric-id":4885878,"id":"Q4885878"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c9d2a23a85242a56044340e0a58cf8a72c5bf622","datavalue":{"value":{"amount":"+0.6880168914794922","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":"Q1334901$AAA27FB0-66C3-4439-9A42-264901DA7BCF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"13124693e0ef4fa81acf6e0fb9c92d3e368683c6","datavalue":{"value":{"entity-type":"item","numeric-id":2723930,"id":"Q2723930"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b9d5ba29e77fb073cde313f8412eff1e4e5c9b12","datavalue":{"value":{"amount":"+0.6870211958885193","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":"Q1334901$D1CB587F-2E73-462F-B8A6-4F23EF63D239","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Annotations in formal specifications and proofs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Annotations_in_formal_specifications_and_proofs"}}}}}