{"entities":{"Q689289":{"pageid":691138,"ns":120,"title":"Item:Q689289","lastrevid":47204614,"modified":"2026-01-01T00:13:49Z","type":"item","id":"Q689289","labels":{"en":{"language":"en","value":"On the status of proving program properties in effective interpretations"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 445057"}},"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":"Q689289$AD5DE2BF-57F7-4473-B91F-4838E638E7A6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5b77fa0c614c8eda824f0f506b265e73dc33a72d","datavalue":{"value":{"text":"On the status of proving program properties in effective interpretations","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q689289$8179323E-952C-4F36-B57D-7B4594597859","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ed80bb30d8cc766a678986c0831b7dc2ccf1d9e7","datavalue":{"value":"0809.68086","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q689289$BFA01DC5-E2F5-4F81-9017-CA726282DF79","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d59f17cd9335c68eb3d5a97ce1fb98daafe1f1af","datavalue":{"value":"10.1016/0304-3975(93)90245-O","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q689289$F0A1658C-EC50-491E-86D0-74A04AEF0CA0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"80918d07e2444d7026e4c565b9b730b5c917c4b8","datavalue":{"value":{"entity-type":"item","numeric-id":689287,"id":"Q689287"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689289$87200B84-E5E9-495C-92E7-62D49C865663","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689289$3A900A26-0037-44BB-9EED-5A009DAB4C09","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"151ac7ed6fc6633f65d3ecb847dedba552bce936","datavalue":{"value":{"time":"+1995-03-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":"Q689289$8C20B164-75F1-4786-8157-466F593AFB4A","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"b039dc34acd4a4aea9cf2948cd938beb34ddf665","datavalue":{"value":"The paper is based on the previous published results of the author. Considering dynamic theories, the author tries to give a generalisation of Lipton's theorem (R. Lipton: ``A necessary and sufficient condition for the existence of Hoare logics'', Proc. 18th IEEE Symp. FOCS (1977). The idea starts from the fact that every proof system for program correctness yields an enumeration procedure for correctness assertions. The effective interpretations are given by recursive subset of \\(\\omega\\) and recursive functions and relations. The paper presents a sufficient condition for a uniform procedure enumerating dynamic theories of interpretations. If arithmetical notions are first-order-definable by universal or existential formulas within this interpretation, then there exists an appropriate uniform procedure.","type":"string"},"datatype":"string"},"type":"statement","id":"Q689289$DAE61DBD-E961-48C9-A168-CB2966C616FD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q689289$4E3B9DD7-891D-409B-8046-B3EA17558B99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q689289$81E4DB67-FBD0-420F-958C-5635789CF530","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1267197712a0b8481bdd51a65bbac0428b08dd13","datavalue":{"value":"03D45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q689289$87956E65-55B2-428D-AED4-00165EEF0A8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"31eb4b2fe460225d8220386b6d12b964cafd1ca3","datavalue":{"value":"03C62","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q689289$D5CCD96A-6B6F-4835-8D40-73E5D6ED2205","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4cedff2262f9f1137e60305951d2980555d09da5","datavalue":{"value":"445057","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q689289$FE1530CC-A36A-46D4-BF07-1257C134B967","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a2b746efc66121bc1fb497da4ab39b83b5cd2f4c","datavalue":{"value":"program correctness","type":"string"},"datatype":"string"},"type":"statement","id":"Q689289$4543E4A7-6DCD-4868-BC4D-EFFD9EA1C128","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c117b0dec2cd1b7dca5d2b6234632939a47fd44e","datavalue":{"value":"theories of interpretations","type":"string"},"datatype":"string"},"type":"statement","id":"Q689289$9C1CCB91-659A-47F9-8E26-93BD145999FC","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"a15109437d833303a14fd0218e3039f04ef1e62d","datavalue":{"value":{"entity-type":"item","numeric-id":264537,"id":"Q264537"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689289$AF8B7371-9743-481C-9A5C-4AA06C423FF1","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":"Q689289$8DCBF1A3-B44D-459C-BD42-EABB519E52CC","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b3bc80122c3248b7370a66f915205122d19550f7","datavalue":{"value":{"entity-type":"item","numeric-id":3925144,"id":"Q3925144"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689289$A015AD1B-F1D8-4BBF-874B-51D988ECF627","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"896a4e1608ded66dec0047e42ace35f2bb27df8d","datavalue":{"value":{"entity-type":"item","numeric-id":3763566,"id":"Q3763566"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689289$D9E627BA-3CF3-4FE4-8A66-27EA63EEADB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e8e9de10892cbf49d39c44126c1348d5c54ef8f8","datavalue":{"value":{"entity-type":"item","numeric-id":3711743,"id":"Q3711743"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689289$C94B4429-79B3-4A97-8C45-DEA00B746C15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"30ae93a4207b1c2e5b3fd93e9358659153a4c7f3","datavalue":{"value":{"entity-type":"item","numeric-id":3765226,"id":"Q3765226"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689289$EB386B82-4890-4590-B5EC-95435DA17C37","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2f7fcdab9e9a73bf77631ca488c65c2b318c669f","datavalue":{"value":"https://doi.org/10.1016/0304-3975(93)90245-o","type":"string"},"datatype":"url"},"type":"statement","id":"Q689289$364123ED-4094-4F95-8281-85507274054A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"dbe84a54c9d97f831b9e466d04a7700e1c1953bb","datavalue":{"value":"W2061285801","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q689289$DAF02853-08EF-4B96-9C72-F38669766FE2","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cce7bdad2532f4d7df7db035258fed4015030a55","datavalue":{"value":{"entity-type":"item","numeric-id":760793,"id":"Q760793"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"859c6287e4c026549e7b98c460e7a70ab5a2fd02","datavalue":{"value":{"amount":"+0.7449702024459839","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":"Q689289$9A2978CE-FF9B-4430-9319-58D6A35CD01E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"672d995dd3428eb07ed30b7429a38292a5821170","datavalue":{"value":{"entity-type":"item","numeric-id":3763566,"id":"Q3763566"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a4eab64ce3f9c76d9e96b027832e908034e27ffe","datavalue":{"value":{"amount":"+0.7422196269035339","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":"Q689289$90B3C358-E81C-4E03-911C-339C31DFF5DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a84e644170331a6a9485b207c047e686cd4d5525","datavalue":{"value":{"entity-type":"item","numeric-id":3826528,"id":"Q3826528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c1b04f51502b3067d0c05821dace4a701f76ed06","datavalue":{"value":{"amount":"+0.7230110764503479","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":"Q689289$07C487FD-E2F0-46CD-93EB-9BCD8DA852BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b033de07e3d56708ecacab644c5d61e90a196357","datavalue":{"value":{"entity-type":"item","numeric-id":3711743,"id":"Q3711743"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"68302120db021e4acf78b310e39e75d3b85cbbe4","datavalue":{"value":{"amount":"+0.7228518128395081","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":"Q689289$0C14049C-CA30-48F8-804B-787DA65231EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"51262ac56a18dec16fbac760c9f4aba47e0e8bc0","datavalue":{"value":{"entity-type":"item","numeric-id":4899919,"id":"Q4899919"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0121cb1381af84c4d3639bc345d26c2b14a6eec1","datavalue":{"value":{"amount":"+0.7136793732643127","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":"Q689289$392067AC-69BE-4541-A6F6-0C84119BCE96","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:689289","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:689289"}}}}}