{"entities":{"Q3585033":{"pageid":5614937,"ns":120,"title":"Item:Q3585033","lastrevid":87471719,"modified":"2026-06-04T11:45:59Z","type":"item","id":"Q3585033","labels":{"en":{"language":"en","value":"Encoding Circus programs in ProofPower-Z"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5776608"}},"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":"Q3585033$DD691062-F31A-4C66-8CB0-4C6C1D0F7FE9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5727fee5e6c3103caec6bc19cfe3fed5435d4aaf","datavalue":{"value":{"text":"Encoding Circus Programs in ProofPowerZ","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3585033$AF833113-CFF9-4311-906B-020EEDA5C69D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"aca7388a0480929cb5c1c6c9e01cd0e4d4350060","datavalue":{"value":"1286.68097","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3585033$5E88C028-B1F5-4CF9-A642-9989F8087E86","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e3a25bbba4faaf90f8341ecac7f731c6a142c1d8","datavalue":{"value":"10.1007/978-3-642-14521-6_13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3585033$D816CB8D-79BC-4202-A709-2D456049FCD2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e4d150d5bf876b5a829b43934d70c20b18c58f39","datavalue":{"value":{"entity-type":"item","numeric-id":432149,"id":"Q432149"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3585033$57123F95-61BD-460D-B965-71A3F66CDE8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7f27d31a7277a70c7762a067d64f6707ee9b1ea6","datavalue":{"value":{"entity-type":"item","numeric-id":315300,"id":"Q315300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3585033$CF1D62F3-C6D9-45C0-926E-2F0588C5AD17","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a469690149bc3cf60335251215f8201e92d3e50c","datavalue":{"value":{"entity-type":"item","numeric-id":2814611,"id":"Q2814611"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3585033$1280877C-C2DD-4EBB-BEB2-0FB8D59427F2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"eb30be9aa52453b28e16b3393b2ab68c6420e54e","datavalue":{"value":{"time":"+2010-08-31T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3585033$11761713-8ABF-4A5E-A29A-E3C396A353E3","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3585033$47D0327D-5241-4006-8CCC-8852ECB25C47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3585033$D1E74783-1632-4523-A2AE-6316DAC15D68","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4181e0cfed49085ee46203d1931f7035b9177985","datavalue":{"value":"5776608","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3585033$E3D8EFA6-77DD-40E7-9030-2B3F26B41239","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"03a0d2848f7e13e5373d661d808855d0d8662087","datavalue":{"value":"UTP","type":"string"},"datatype":"string"},"type":"statement","id":"Q3585033$280F56A6-A6EE-4D43-B61F-6C539B54BC72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d7bfc11de8cab95fd6af201970bd9d16d39bbd0","datavalue":{"value":"semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q3585033$E476BA06-E28F-449A-9CE3-069737D6AB87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"30fafc44265dfa91ca2c1422c4fc2ccc0afa28bf","datavalue":{"value":"Z","type":"string"},"datatype":"string"},"type":"statement","id":"Q3585033$EB8C0F15-54DF-4ED3-ABE2-0944873D4304","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q3585033$81482284-931C-4A91-AE3E-E64050B12C50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ab20a0363e682206851b94b3be1e96bb56399f58","datavalue":{"value":"refinement","type":"string"},"datatype":"string"},"type":"statement","id":"Q3585033$1B9A46E6-A531-49CE-87A7-61DB577C92BC","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9189048b3936abda7e80b02cf829681849623735","datavalue":{"value":{"entity-type":"item","numeric-id":33628,"id":"Q33628"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3585033$E10C675E-CAC6-4597-9EC5-422AA64D73BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"dc27975e97e4cd38daedfdbb9f73615febe95f84","datavalue":{"value":{"entity-type":"item","numeric-id":18466,"id":"Q18466"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3585033$7C8F64C1-E8D5-4613-A2D1-94B3A0301799","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8b2040a476017b43b21bd352cfec0a67d631d6d4","datavalue":{"value":{"entity-type":"item","numeric-id":18467,"id":"Q18467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3585033$ED799B62-FAAF-42EF-8748-6B281A27E83D","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":"Q3585033$926C7BD0-E961-4D9A-A586-6297C505B2AF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6361acc0e389677a869e08480cddaa06d4602bd5","datavalue":{"value":"https://doi.org/10.1007/978-3-642-14521-6_13","type":"string"},"datatype":"url"},"type":"statement","id":"Q3585033$17AD5C21-3AB0-4EF8-BDA0-3F2727E0986C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0952bab622ee39c4030e3cd3100d9720991ece58","datavalue":{"value":"W1579044745","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3585033$1F04BD2A-0111-4E8D-B39A-B65A3BA3B94A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f9a3a7bd6f648ff266352564b47deffbfbb84804","datavalue":{"value":{"entity-type":"item","numeric-id":2999326,"id":"Q2999326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4633c07c9ba070babb4a370a878374fd62d31a05","datavalue":{"value":{"amount":"+0.8409897089004517","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":"Q3585033$978D07C6-09F0-4744-B4C5-E94696F3606A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8c00d6b98765156e0ec29101db3b1772bc2b3dc0","datavalue":{"value":{"entity-type":"item","numeric-id":1019016,"id":"Q1019016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c1b35e771a4eabddb1dd5877bae1abfd026601d9","datavalue":{"value":{"amount":"+0.8322590589523315","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":"Q3585033$CAFE30AE-E9F1-44B4-97AE-1ECCF1FDC838","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fdf6128767f41e8247a95055a64d5113ae336cd3","datavalue":{"value":{"entity-type":"item","numeric-id":2873610,"id":"Q2873610"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"83f14b071ecbd2390c8d1147e6e24d9ed21c97bd","datavalue":{"value":{"amount":"+0.7793159484863281","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":"Q3585033$FECDAFD4-61C0-4E4C-A42A-BDBF8F759381","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"00a750499399fb23693a151d13210daf45e5912f","datavalue":{"value":{"entity-type":"item","numeric-id":766162,"id":"Q766162"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"43a407082c171ab75bf94f2f99e64f27b4eac560","datavalue":{"value":{"amount":"+0.7770812511444092","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":"Q3585033$13CFDC59-BEBF-471D-A975-5461C63B36A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4a73c88cae8fa0a228995f00f01a8b5461832bfc","datavalue":{"value":{"entity-type":"item","numeric-id":1941892,"id":"Q1941892"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2f0455b92fcef499e65fde85834fb55a3fa850d1","datavalue":{"value":{"amount":"+0.7755084037780762","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":"Q3585033$B4FB0F41-CEBC-463D-BED2-A816AC3A0110","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Encoding Circus programs in ProofPower-Z","badges":[]}}}}}