{"entities":{"Q843604":{"pageid":845452,"ns":120,"title":"Item:Q843604","lastrevid":50878424,"modified":"2026-01-15T13:30:43Z","type":"item","id":"Q843604","labels":{"en":{"language":"en","value":"Proof compressions with circuit-structured substitutions"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5659080"}},"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":"Q843604$F8CE7432-8DFC-4A0D-898A-3774A3D50BE6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c36e89c7476f6440b7e9afd2ff4701b056c8721d","datavalue":{"value":{"text":"Proof compressions with circuit-structured substitutions","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q843604$9085F7AA-1B07-40E5-8B5E-F9EEE82C1866","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5865fd88a18bfbdb3e44b2f68291036104478e3e","datavalue":{"value":"1191.03043","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q843604$61BEE721-CA41-4D16-90A7-BF82B689C7F9","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9e8a835a06760ebbf576944c982d8520ba2f9a83","datavalue":{"value":{"entity-type":"item","numeric-id":843603,"id":"Q843603"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843604$4F0E6C04-B27C-4E4C-AE38-BA77A104C9C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"da91d821e6afd5fc2acad321f0aa06b2e18cae96","datavalue":{"value":{"entity-type":"item","numeric-id":1147136,"id":"Q1147136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843604$5406B7BA-7422-4B3B-A9FC-66B0AF688E9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"523eb1c9f92e29e52a82edbd2df5947e22806cd3","datavalue":{"value":{"entity-type":"item","numeric-id":281153,"id":"Q281153"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843604$D18ABAFC-63C6-4AA2-BC97-10EF4BBB238E","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"17c447c8e76a3a0e73a2c70a024d9ee2f8256c04","datavalue":{"value":{"entity-type":"item","numeric-id":195577,"id":"Q195577"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843604$A4ABB46F-5ACF-44B1-A5C7-5EC301630A3D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"8f6c5227c532f1642a28ac5ec57c91ab7b824960","datavalue":{"value":{"time":"+2010-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":"Q843604$92D0AB36-A0B8-471C-A6C5-D5470B089B76","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q843604$6CBAEA87-6EE1-4F89-BEE7-5AF6967D135E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q843604$A26E0F9B-36D9-42A0-98D1-ECC8857DBDD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q843604$A29E25B6-3EED-4E7C-8FC7-EBDBF13D2BEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6e2ae8b1900147d15ddea62ccb5302a15ee19b5d","datavalue":{"value":"03F07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q843604$2E15D587-A4D3-4C8C-9CE9-246503CD8190","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e41e4c43d856bdc796a2f2b02e6498e6e35b2a99","datavalue":{"value":"5659080","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q843604$4EED3F64-4B3F-4A67-8E3A-71CD2BF1A410","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d54d530443288b6d91131d0a2e0caa5ce4779c88","datavalue":{"value":"proof size","type":"string"},"datatype":"string"},"type":"statement","id":"Q843604$0DB6387C-50D4-443B-91E6-C58F2AC1B061","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9d2aa687cef17cd912aad76972cec097c0540be8","datavalue":{"value":"automatic theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q843604$89706A05-54BC-4650-8E57-B746BCB9750C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2cb69ef676f7a366490397a06d8bbfd575a8dbe8","datavalue":{"value":"atomic-cuts proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q843604$6B45EB3C-AC98-4F9C-98EC-9616C9EF2A96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6bd34074526ff9d5d53722d72ef57f42fa801ea2","datavalue":{"value":"cut-free proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q843604$40EDC9CB-C7B3-421A-8000-DBCACEB8A3F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"97e8b8540955bb432519b936aa7417c2dcecc080","datavalue":{"value":"circuit-structured deductions","type":"string"},"datatype":"string"},"type":"statement","id":"Q843604$5014EF1F-C434-47F0-B82E-651ED06DC5EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c3922eb0b8235fb2b824bcb3eaa0c8d395dbd512","datavalue":{"value":"unification","type":"string"},"datatype":"string"},"type":"statement","id":"Q843604$0336C5C8-AF55-4665-A4F0-81DC4E31CDF4","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":"Q843604$8C0D876B-D1C8-4630-933C-D6F929AA7806","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4a32a354b9ac66c92f71815406381e55c515e049","datavalue":{"value":"https://doi.org/10.1007/s10958-009-9405-3","type":"string"},"datatype":"url"},"type":"statement","id":"Q843604$D9FB1AE9-5E43-4A58-99FD-DC7130E9E5E9","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a7dbd188c2230094989db026aa8a46dcbe39a0e4","datavalue":{"value":"W2073542215","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q843604$D16B9479-9E61-4B5D-8543-F31E36D8FAD2","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0086f5e874fe7e4f38ea6905507c6d71ae7ad220","datavalue":{"value":{"entity-type":"item","numeric-id":4399249,"id":"Q4399249"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843604$893D318C-0279-47B6-8829-ACD0DD921444","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f31cbeafb74eb2331031a6d2305fa02411af3e7","datavalue":{"value":{"entity-type":"item","numeric-id":3775553,"id":"Q3775553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843604$A45EA54E-3C40-48EA-A632-EDD1A9114AEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bbf9a6f410239e7440737c16f5b97b7808eb6e02","datavalue":{"value":{"entity-type":"item","numeric-id":4513125,"id":"Q4513125"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843604$FD627000-EC30-43F2-8E60-30FD0C2E8D8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f174f8187c91bfe6499d7c38885f45afea642586","datavalue":{"value":{"entity-type":"item","numeric-id":3007263,"id":"Q3007263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843604$05AAF761-5B07-4A54-A713-EF3C5FBC1159","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"53674086d0b747bcbbd79e06734f8da013fe9ed3","datavalue":{"value":{"entity-type":"item","numeric-id":3781102,"id":"Q3781102"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843604$F2F2B260-789A-4131-A309-376DFCAB08B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec2fa04d400281f100817ce7e13bdaafd2683670","datavalue":{"value":{"entity-type":"item","numeric-id":1071750,"id":"Q1071750"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843604$5124CAD5-11B3-4852-9AFA-36113E9D6242","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6e8f21ae813780ffb1b14b622d2c99e2bf7de1d2","datavalue":{"value":{"entity-type":"item","numeric-id":1254248,"id":"Q1254248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843604$C3CC665A-356C-4322-B4F0-E490813400EB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a8134f270e9c1873f12a69c90be3c8567040b341","datavalue":{"value":"10.1007/S10958-009-9405-3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q843604$2F29144F-5A39-459B-BD90-A6021E0F732A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"04fbecbabdd68f481aee5847d1d9e0118e410ae7","datavalue":{"value":{"entity-type":"item","numeric-id":4283227,"id":"Q4283227"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"784fabf086b4b48481c7b8d51b5df823100d706a","datavalue":{"value":{"amount":"+0.7822494506835938","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":"Q843604$59BFC34A-43E9-4AF8-BD42-C15AA2708088","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5fe186cac75804def3c2fa703a831734e4da013d","datavalue":{"value":{"entity-type":"item","numeric-id":5361251,"id":"Q5361251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0901a9d1ddb9547083a9bd7ff69c09f96eeda12c","datavalue":{"value":{"amount":"+0.7808516025543213","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":"Q843604$BBFC149E-5148-4F92-991E-8A5F4279C793","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9e01a1a87e9e21661fc2d247dde7f3d538b8883f","datavalue":{"value":{"entity-type":"item","numeric-id":2631644,"id":"Q2631644"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"038b44aecc25c80ea8d815b21d26ef00aa02c2a5","datavalue":{"value":{"amount":"+0.7784397006034851","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":"Q843604$D2DDD5AB-7468-4718-BED7-41F9CD63C9A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8eff3dd9b05835796a1c0aadcfa0552a9eab1a79","datavalue":{"value":{"entity-type":"item","numeric-id":3066113,"id":"Q3066113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7558aea51ef19c4f1d3c4e02091f8a0f890a92b5","datavalue":{"value":{"amount":"+0.7746545672416687","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":"Q843604$C953A76B-B54C-4534-B376-E0CD27423C22","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ce2877963848044aafe30ac36ae6e1ad563d9d1f","datavalue":{"value":{"entity-type":"item","numeric-id":5039194,"id":"Q5039194"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0c85b9c172f9cca0e0fb3c9a51fa1d35125db06c","datavalue":{"value":{"amount":"+0.7705730199813843","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":"Q843604$E78FAC43-9F2E-4E58-A21B-632547EAB736","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:843604","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:843604"}}}}}