{"entities":{"Q5164172":{"pageid":7193743,"ns":120,"title":"Item:Q5164172","lastrevid":58463952,"modified":"2026-04-05T08:15:53Z","type":"item","id":"Q5164172","labels":{"en":{"language":"en","value":"What's decidable about program verification modulo axioms?"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7423372"}},"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":"Q5164172$4321FB3D-154B-452D-AF8A-DB180E1317A6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"529b950461619a42aaba604a2dbbecd6e6572449","datavalue":{"value":{"text":"What\u2019s Decidable About Program Verification Modulo Axioms?","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5164172$DB79E06C-07CB-44CF-A27F-02BD46E3898D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3643ebf3d9fc76d855d9f77afb99b35b7f2c64ac","datavalue":{"value":"1483.68200","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5164172$151D22DC-1218-4118-A8E6-FC7914F5DEDC","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3d1756961144b91b7d5ec84e67f9718fbaad2e43","datavalue":{"value":"10.1007/978-3-030-45237-7_10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5164172$FA6E3F05-0B81-47FC-9BD7-DAFE482EEECB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3832a6f49368bc25104676db11d18b956393ba53","datavalue":{"value":{"entity-type":"item","numeric-id":2164213,"id":"Q2164213"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$6F175C37-F55D-48CB-B41A-5FA466CF9D2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ed7ae23aa61a0d3617ed945c3a7817f6e39ebeb8","datavalue":{"value":{"entity-type":"item","numeric-id":236078,"id":"Q236078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$184A79A0-C99C-49F8-8784-13560C18BB23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"143b6b92bc6a16b35c1b93aef5aca0ebdc691790","datavalue":{"value":{"entity-type":"item","numeric-id":650913,"id":"Q650913"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$9EEDB83A-8572-4B6D-8FB6-2BDFB364090D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"0caef843b05c7cfb5667c1a8106613cbf61a6d23","datavalue":{"value":{"entity-type":"item","numeric-id":2894263,"id":"Q2894263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$39BB5BD0-CF88-4C64-AC07-F33135B699B9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e41df14f190dd9eb0cc664848f84d930123fd453","datavalue":{"value":{"time":"+2021-11-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5164172$2F5D5542-6D50-424A-83FD-9610A8C1D39C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"650a575c886786ccecdc0483971d70a69120a876","datavalue":{"value":"https://arxiv.org/abs/1910.10889","type":"string"},"datatype":"url"},"type":"statement","id":"Q5164172$7A285E39-C21B-41FA-91A6-B3A5719FBF72","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5164172$0CAD84CF-2187-4465-9C6F-70338532EB6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5164172$A4102965-010C-46BE-AFDC-4F2451907053","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5164172$E96B38C7-BB37-4349-B30C-446A7305764B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"134afc84a011046ca091841a8227c55d77e8fa10","datavalue":{"value":"7423372","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5164172$CA8E2863-3ADF-4707-B461-3C3E299D8238","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"cc58ad0645335839a7be6fcd1c3c5700ae701897","datavalue":{"value":{"entity-type":"item","numeric-id":13549,"id":"Q13549"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$F3FEF31C-7F8B-4032-961E-939064CFEEC6","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":"Q5164172$D6DB558D-3809-4BB0-94DA-F4868D9B9987","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"fd35efda4432dd96cd64723337d20ea5cb1b3f7a","datavalue":{"value":"W3021960956","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5164172$5C338432-A45C-4DAA-952E-A1F6A5B9977F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"039ef2715aff948a023b817faf30cce195da0a45","datavalue":{"value":{"entity-type":"item","numeric-id":6041167,"id":"Q6041167"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$1D88B071-71F1-4523-BBA0-304CC05A40CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7489661d0c92ad040adf8d2140d5b6efc776b644","datavalue":{"value":{"entity-type":"item","numeric-id":1055450,"id":"Q1055450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$0829A93D-2FDC-4F9F-B5CC-E3937426FE25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84339eb1b9200fd0bfaec4876ec88a12251ced16","datavalue":{"value":{"entity-type":"item","numeric-id":4919632,"id":"Q4919632"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$5E92362D-8897-45FF-A60D-AD420A69FAEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f4906fd8042c8865b223243d5b906328c24e54d","datavalue":{"value":{"entity-type":"item","numeric-id":2848689,"id":"Q2848689"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$03A609D1-5ED9-4D6B-B929-F42C635B5337","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"adaf08cc2d75d40d9af63f2dff7037cce33c5f56","datavalue":{"value":{"entity-type":"item","numeric-id":2828258,"id":"Q2828258"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$6FC7F353-165C-4A5A-8DC7-8FC8FF443CF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f232357ea33a81e1500bd1c1fdcc1712a44dbf5","datavalue":{"value":{"entity-type":"item","numeric-id":5711512,"id":"Q5711512"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$1BD8619C-84EB-46DA-88CF-D2EC61C259D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7c5cea71c6aacfcb4cc8bc4d70a2c543dbb0d272","datavalue":{"value":{"entity-type":"item","numeric-id":5408550,"id":"Q5408550"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$21E9D53E-C971-4B86-B07B-4619F0DCCF38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d6e5a2ec66a572177ef7c34d7ff9e3c5a3050d5","datavalue":{"value":{"entity-type":"item","numeric-id":1157324,"id":"Q1157324"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$ECD68720-DD30-418C-8800-FB0C81450F89","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e4be82556f4392c3a11aabb4e7e7b5078ed0ae9f","datavalue":{"value":{"entity-type":"item","numeric-id":5167845,"id":"Q5167845"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$84E3FD3B-717C-4618-9713-25E9EFD2860E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"807ba00199ace6f7367558f06f230d3484fc77af","datavalue":{"value":{"entity-type":"item","numeric-id":4362921,"id":"Q4362921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$95B1561E-09DE-49F6-A8AF-78671BC07ED9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8b108d2635a4984b52da5032144326036106766b","datavalue":{"value":{"entity-type":"item","numeric-id":5408433,"id":"Q5408433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$FF42233F-98AF-4378-9AE3-0D86EF8CAD18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fcf2b678c67af5d9c3ef01ce8f5125a52e30717a","datavalue":{"value":{"entity-type":"item","numeric-id":5255103,"id":"Q5255103"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$D470C4B2-49A2-465E-B368-6CC6FC7FBF15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"acde43aadb68c83ae4d51574dcef8cc0958b2d7d","datavalue":{"value":{"entity-type":"item","numeric-id":3392921,"id":"Q3392921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$9DF8323F-6459-412E-ADE7-7E224EFD01E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1774dfe4960a0840f2ba7e2e9f290bbde1f75301","datavalue":{"value":{"entity-type":"item","numeric-id":5452620,"id":"Q5452620"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$A892DF01-790F-4115-8460-3EAA59F11DB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7c6740f14e87c03ddb72e412a6af226124af4cf8","datavalue":{"value":{"entity-type":"item","numeric-id":3392933,"id":"Q3392933"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$0367C3D6-E991-4A79-9054-BB1C35614C35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"50857a8f041a6c593aa9ea3f6304a3ab1d297bce","datavalue":{"value":{"entity-type":"item","numeric-id":2819827,"id":"Q2819827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$84F02769-B558-40DE-9888-5209CD4CBFE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dfe368fb0b8f14e62aa960d3e2359d02cf4413f8","datavalue":{"value":{"entity-type":"item","numeric-id":5408413,"id":"Q5408413"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$250257DE-D5E0-4FF3-A265-22B6CF146AD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bbb01f51aac999eba17cc3ca784f571a7357214f","datavalue":{"value":{"entity-type":"item","numeric-id":2931789,"id":"Q2931789"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$35173DE2-0DE4-47F3-B13C-9FD3E3C7E1D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e6abd173db405d6471938fbd375158ea21bafe9","datavalue":{"value":{"entity-type":"item","numeric-id":2289074,"id":"Q2289074"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$D5D17A80-F4E4-4F74-8D7A-ED418A44EC8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fe57e8b9b6906da78f6a53223fb638828120e81f","datavalue":{"value":{"entity-type":"item","numeric-id":2819794,"id":"Q2819794"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$0D932029-61F1-4FD9-AA79-91CEB6994D0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6e44aa8c15f122662072cb1a33dba6371f47f798","datavalue":{"value":{"entity-type":"item","numeric-id":2828317,"id":"Q2828317"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$5C59120A-1F51-4848-8D82-1D31E6FA9273","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0dcaa4e05eedac47584d8837dfe028b566df5257","datavalue":{"value":{"entity-type":"item","numeric-id":2287098,"id":"Q2287098"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$D024F167-314A-4BD7-BF26-4C4A09D0A5F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0e242557b370e70ca22794bd752775ec0bac8856","datavalue":{"value":{"entity-type":"item","numeric-id":4804887,"id":"Q4804887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$8F2884FC-132F-4608-8719-97B3EF776810","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"af6385968bdd813161bac6e71c7cc845350a4a9e","datavalue":{"value":{"entity-type":"item","numeric-id":5429330,"id":"Q5429330"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$9ABBB54B-BACF-41AB-B6A5-174589621E7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1e8ee0155f93c9dd7091efbfd761c9afcd16248b","datavalue":{"value":{"entity-type":"item","numeric-id":5505565,"id":"Q5505565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$711EA3E1-D801-4B63-896D-F3AC8617E48F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"be10dd9c5244947afed4301a642cfca828375156","datavalue":{"value":{"entity-type":"item","numeric-id":2226763,"id":"Q2226763"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7d9aa97e74af725ebc388eae878d2e22d131bc7d","datavalue":{"value":{"amount":"+0.7735130786895752","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":"Q5164172$0E44257C-6ED9-4C6D-BCAB-7E70DB2B90F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f82b1d2a82d3363778068033fd9d39512b52f9f6","datavalue":{"value":{"entity-type":"item","numeric-id":3075488,"id":"Q3075488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"51eccec18f9c3be676a90187754ef8ebbbac48c3","datavalue":{"value":{"amount":"+0.7324422001838684","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":"Q5164172$BC142E85-3D55-469F-808E-C78ED8D0812D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e3ec55ae651c94a18007aafb265d66f89e568dbe","datavalue":{"value":{"entity-type":"item","numeric-id":1091795,"id":"Q1091795"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ac119352a444363b8f1597701988b87ab7d87b63","datavalue":{"value":{"amount":"+0.7242226600646973","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":"Q5164172$AF0E73F2-67D3-4E0A-9E82-138CFD5B6584","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1063bece29dd4b6e998e94b2f0084b7f2a844456","datavalue":{"value":{"entity-type":"item","numeric-id":5898633,"id":"Q5898633"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4d6520fd67132aa42000d2621bf8033ba64a3e3e","datavalue":{"value":{"amount":"+0.7134608030319214","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":"Q5164172$F5370324-2686-4C3C-8A59-D58B52C78535","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"107c509c827589280206681f81dfd6a2a3d078a8","datavalue":{"value":{"entity-type":"item","numeric-id":5168511,"id":"Q5168511"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fa546bb199450a3bf173a7450eb28e77d9471f7d","datavalue":{"value":{"amount":"+0.7128711938858032","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":"Q5164172$D763A0ED-9B9B-49F0-B200-BA9E87AB9C58","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5164172$3F21CA57-AE37-495A-834B-0E73108E7EC5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5164172","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5164172"}}}}}