{"entities":{"Q4647514":{"pageid":6677095,"ns":120,"title":"Item:Q4647514","lastrevid":97925108,"modified":"2026-06-05T15:49:20Z","type":"item","id":"Q4647514","labels":{"en":{"language":"en","value":"Mechanical verification of mutually recursive procedures"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7001906"}},"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":"Q4647514$7089C516-72A7-4782-9254-8D2058C2064A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f4cfc0d28f4b3f6edbab9fff1d558db3532e9972","datavalue":{"value":{"text":"Mechanical verification of mutually recursive procedures","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4647514$ECB86C84-9206-4520-9C3E-1A09BE7B6821","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"65918ac600193c5c492f23f3dc8cc3ff0ab5578a","datavalue":{"value":"1412.68138","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647514$6EF7668F-7289-4066-9F85-35FFA890D047","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5ef505148f1a7b298a5c368a13d4e6ba149ec9c2","datavalue":{"value":"10.1007/3-540-61511-3_81","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647514$F5F35310-A8EA-49E9-92A2-6CF78AAE009F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"30571cb690398849c0604e122d31faa0b2492672","datavalue":{"value":{"entity-type":"item","numeric-id":1887134,"id":"Q1887134"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647514$62777C50-74E4-4555-844F-3A30370283ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6cbff9cb0a6dcc21882cd61445624ac87c8bb4db","datavalue":{"value":{"entity-type":"item","numeric-id":1887135,"id":"Q1887135"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647514$74D312FA-AACE-4528-8985-3460C0D66530","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"1c1c5ae1cd90ac8f2e7ae6528ac21a720bbd1fe8","datavalue":{"value":{"entity-type":"item","numeric-id":4647495,"id":"Q4647495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647514$5B8E4E01-BE81-4C78-A19A-B46773148B3E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"250f083a2ef1e7a7df79afad0acdd22e5799ecf5","datavalue":{"value":{"time":"+2019-01-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4647514$08BEDAA0-5E3B-407A-9876-04EBBA0B78E5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647514$38173E86-226F-415B-8726-50804C1977A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647514$1FB53B18-6813-4DA9-B845-CB8B3FEA3618","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"01f467b1c250ee7c9786930b333799b0f400250e","datavalue":{"value":"7001906","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647514$AFD60327-8C43-40A9-A134-84BD3BCC825A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"64313dda4359e47c654b65cb9e6f480a31977931","datavalue":{"value":"logical variable","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647514$3394FDCF-B5C4-4562-975B-CB91D1202C65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7446a8683987eff8e607ef8f5e32e3d98001d893","datavalue":{"value":"recursive procedure","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647514$2A14AE4E-27D9-40C4-9D75-9BC9C7C1E9FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"82c57f1aef24e8b9bfd4065665df523e5193ac40","datavalue":{"value":"Boolean expression","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647514$E221EFCE-7AAA-4836-9413-F0C0E536827A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d787c51842fd919c4ff40c6cb9273f8833ce7fa4","datavalue":{"value":"individual program","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647514$D3C77233-EFFD-48B3-9265-F37724B8A34E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8c28c3110903eae6a23631aa23fc93dc8c530c8a","datavalue":{"value":"verification condition","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647514$2A5D822B-E578-4345-BC6A-3C7D64D619C3","rank":"normal"}],"P1463":[{"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":"Q4647514$37AD1238-0C88-40B4-B06A-DB4C48E58B8E","rank":"normal"},{"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":"Q4647514$5E363F42-2631-4CF8-AAF8-69F914CD2823","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":"Q4647514$2B72814F-492A-47E7-80AD-5F7DC43582C0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e679c949b4ce454252cca4f12aa8a476d9b32883","datavalue":{"value":"https://doi.org/10.1007/3-540-61511-3_81","type":"string"},"datatype":"url"},"type":"statement","id":"Q4647514$6F14AB51-EFE5-4548-A0F2-275732A1E428","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0239dc55cd44c4bf05a6e5e3cd797c438598758d","datavalue":{"value":"W191371315","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647514$D437C0DA-F4FD-4CBA-9C82-5C4A08782363","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"e2c71c26bf7e075dc23cee40b3135f1af13e67a2","datavalue":{"value":{"entity-type":"item","numeric-id":4151703,"id":"Q4151703"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647514$CA764E6E-8725-476D-9A43-D7AEF1001CB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df6d745c28f41f3f6887e89cc1ca892988e70309","datavalue":{"value":{"entity-type":"item","numeric-id":5287513,"id":"Q5287513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647514$12914C32-9A28-4754-89AE-4C9C2F11E34D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"18b7e8541b8bf7dc514993aa6ba095a6f824bbca","datavalue":{"value":{"entity-type":"item","numeric-id":3922131,"id":"Q3922131"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647514$F0B31FBF-2B3C-4A8E-AB23-C361B6EDA293","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d5e10e9078af77fb1b514c3322c4c3e09d63456c","datavalue":{"value":{"entity-type":"item","numeric-id":4151142,"id":"Q4151142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647514$8F8716BC-F6EA-46D3-B42B-CDC3E926772C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f28430ed9b4f7a26aeb0f032922db74966365595","datavalue":{"value":{"entity-type":"item","numeric-id":1843170,"id":"Q1843170"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647514$D0BEE2E3-A84A-4DAB-8365-A0601BD0F0DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d1ac7b93b3fb904267542dbd0727427e6a4861bd","datavalue":{"value":{"entity-type":"item","numeric-id":3912005,"id":"Q3912005"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647514$315866F9-AF2D-4052-9D90-E3E6F0A9B55F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"06bb1394bd77e254671df96ee4ca31515f317d10","datavalue":{"value":{"entity-type":"item","numeric-id":793507,"id":"Q793507"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647514$C9057FC3-60E0-4048-AFE1-02FC4A88EFEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a5f149ec444851c81f8f28cc669b90ac06bcf6ea","datavalue":{"value":{"entity-type":"item","numeric-id":1106190,"id":"Q1106190"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647514$D6F8BA17-BE0F-4809-8AA6-F64F5C56704A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"06c35a02114839df8ec37c9b47eb3fe93b7baaeb","datavalue":{"value":{"entity-type":"item","numeric-id":3141916,"id":"Q3141916"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647514$DDEBA961-8BCA-4399-A044-71284F1E2194","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"47cb83556b7cef6399b3b254f5ad5b10124d3050","datavalue":{"value":{"entity-type":"item","numeric-id":1887136,"id":"Q1887136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"53b58d2c6a11033b76db48eca5431843768e9971","datavalue":{"value":{"amount":"+0.98721045255661","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":"Q4647514$A6EFFDA6-08AE-4768-843E-DFF30E7678DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e4378a70f2913be0b6193290cc8cc54cdad05208","datavalue":{"value":{"entity-type":"item","numeric-id":2912122,"id":"Q2912122"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6d85ac28e25a3e2252708119791c72b42cfc686a","datavalue":{"value":{"amount":"+0.7783532738685608","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":"Q4647514$4342A8E5-2DEE-4CBA-9008-D34F43CF4176","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"562c92cb91f0b2ecd3f6b1b6b8e9d74cd40afb2a","datavalue":{"value":{"entity-type":"item","numeric-id":3012541,"id":"Q3012541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"93382c7c027b4bb03f2d8281b38834a5a750e271","datavalue":{"value":{"amount":"+0.775335967540741","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":"Q4647514$E22B14D4-D10E-4975-91B7-4CE1831908AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"743c51006ea6f95a93c74df5bf1ba99380528b1e","datavalue":{"value":{"entity-type":"item","numeric-id":746783,"id":"Q746783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2b2cbb788004f956e204a856069923203666d1a8","datavalue":{"value":{"amount":"+0.7741255760192871","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":"Q4647514$1E14A0AB-21A3-4B66-AA5B-247DD318CF49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1dde2e2fb41aa5e4499bc3889ab64db327fd2b2d","datavalue":{"value":{"entity-type":"item","numeric-id":732009,"id":"Q732009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9aad933839a0e1e4beea480b4321cfa802f8cc53","datavalue":{"value":{"amount":"+0.7682872414588928","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":"Q4647514$435AA398-DE4B-4D57-BA59-5DA3D2E77C1D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Mechanical verification of mutually recursive procedures","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Mechanical_verification_of_mutually_recursive_procedures"}}}}}