{"entities":{"Q945055":{"pageid":946903,"ns":120,"title":"Item:Q945055","lastrevid":65534559,"modified":"2026-04-12T03:16:19Z","type":"item","id":"Q945055","labels":{"en":{"language":"en","value":"Proof synthesis and reflection for linear arithmetic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5324394"}},"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":"Q945055$3E7E6CA2-D714-4A7D-BBDE-739A5DE73C76","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5cbfd6eca7810022c1a0b72e3f7cd7daeab38f3b","datavalue":{"value":{"text":"Proof synthesis and reflection for linear arithmetic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q945055$9189AA4F-D98E-4DE8-9FFB-EE6B709E87BA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"400e51aaec113e6940b598733bef7509596cc7a4","datavalue":{"value":"1171.03006","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q945055$BBE4BD01-8B2E-402B-8F30-3A65E3C470C2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8c973ae8cb97c26cea9e67d82e7a35f420626e2a","datavalue":{"value":{"entity-type":"item","numeric-id":438551,"id":"Q438551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$32DBB844-0E2B-4AFB-966A-5CCFD2F1DF65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bd39997decddd4925a8ef09cbbffc4f41d2b1f00","datavalue":{"value":{"entity-type":"item","numeric-id":670700,"id":"Q670700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$71F5EE4C-C85C-4F35-9E27-34C59F19BC9C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$92B9D4A2-A194-4EF3-B724-491F8E002F29","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"131b596fa601c3661806f2437747b7af2f563219","datavalue":{"value":{"time":"+2008-09-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":"Q945055$3EBE8B8F-EA99-4C5B-989F-7DAA66C68C7A","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"cf38dfd2756f40e025f51a959d40a6d86ef587f1","datavalue":{"value":"The authors present an implementation of quantifier elimination for integer and linear arithmetic. The algorithms (those by Cooper for \\({\\mathbb Z}\\) and by Ferrante and Rackoff for \\({\\mathbb R}\\)) are realized in two different ways: one \\textit{in a tactic style}, by a proof producing a functional program, and the other one \\textit{by reflection}, i.e.\\ by computations inside the logic. The methods are compared using an implementation in Isabelle/HOL; it is noted that the implementation using the reflective approach is faster.","type":"string"},"datatype":"string"},"type":"statement","id":"Q945055$579EEFA9-1FDD-42DE-B515-B90BBE14D933","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"895d5fc798d777f77a43df1e1b11857e28584cdd","datavalue":{"value":{"entity-type":"item","numeric-id":592080,"id":"Q592080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$D177634F-BD79-493F-A44A-CFF3130111AE","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q945055$6CCD8E2C-1592-4849-A25F-A14016FD3300","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"176e47af9f9e7cf4ebff07fc1f9e4f94a83134c1","datavalue":{"value":"03C10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q945055$B9595118-9A55-4E65-95CF-A79ADB0E071D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q945055$534B80E0-496E-4964-A7B7-C563F132AF90","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1cab5da70f2ea4e609dcf463a35af42361659407","datavalue":{"value":"5324394","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q945055$36432088-A624-46FC-A0BF-71F304C6680B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9072e4a6d9dafd8c8ec2e3f84628a32b8a5ba17c","datavalue":{"value":"proof synthesis","type":"string"},"datatype":"string"},"type":"statement","id":"Q945055$3E65817A-B000-4BF1-8036-EDF4DBF143B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"50b1882775c4720c2bd9796b439d3fd05a08dcd3","datavalue":{"value":"reflection","type":"string"},"datatype":"string"},"type":"statement","id":"Q945055$9BC4F91D-3333-42E8-8A2D-2B5BB2C15C77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"312ed6497197fe722552104318fb5c842ebebed4","datavalue":{"value":"linear arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q945055$6F9714E7-51FD-43A1-9FB6-DB434E690138","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7ce94254d44045733e962d2861c33d94e3725cca","datavalue":{"value":"quantifier elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q945055$AFAB7727-9039-4143-82CC-C16B70FB1D2A","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$A9813CA5-E29C-4928-915E-D0CBB899B28A","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":"Q945055$CD48D5C4-27F8-4CE0-AAEC-0827988EB03D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$257744BE-D95D-4383-AC24-733F4590E919","rank":"normal"},{"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":"Q945055$C79EF602-B6CC-40F8-B0C8-795F0438AC15","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":"Q945055$340CEC72-7088-4A00-9E49-B625154F99FF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e2d7650edffcf2f204148b7bbbb1069edce5ab59","datavalue":{"value":"https://doi.org/10.1007/s10817-008-9101-x","type":"string"},"datatype":"url"},"type":"statement","id":"Q945055$C60C3101-7430-4E04-A815-9EE4C0F3EB24","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"7a756eef6d158889d9d441faed71407aa73221ca","datavalue":{"value":"W2056972299","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q945055$A61A41FC-5BE3-4475-9F7D-4AF3AF163FCF","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"09f9dec41c7615ebddca88a5ee0923f61e9449fc","datavalue":{"value":{"entity-type":"item","numeric-id":1610674,"id":"Q1610674"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$95F9556E-ADBD-4A72-A220-E22A1570FFAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9c60f93a1843fcd9c0656971efa4327b435decb9","datavalue":{"value":{"entity-type":"item","numeric-id":4736387,"id":"Q4736387"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$8C1D1103-73D7-40B0-83BE-5679F08C8536","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d74eec834971a75b92aae841b2c83f9c1a887997","datavalue":{"value":{"entity-type":"item","numeric-id":1159661,"id":"Q1159661"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$EC8ECA29-F337-4077-A5E1-E5998842C1D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f3ea02b15a15931f4cd364dd4a0ce61e10ac225","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$DF8B9F0C-8D73-4B24-B53E-775A2B0B21DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cdf99a4f438802c0f173ce13dc96040bdb8d590b","datavalue":{"value":{"entity-type":"item","numeric-id":3613432,"id":"Q3613432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$F096692B-75A1-4C73-B911-CA078688280F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2be7638796320e0bd21589c519d4a54a0b3ddeef","datavalue":{"value":{"entity-type":"item","numeric-id":5387851,"id":"Q5387851"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$BC2E9EA0-8116-4864-94B7-A23E83B78959","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"648af4444efef3dfface63422920536bd2b0c180","datavalue":{"value":{"entity-type":"item","numeric-id":3928246,"id":"Q3928246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$C28E6E11-6F1E-4B3D-913D-1895D9BB3A65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4d7798eba50e0ffe1e4306d4a4aa338f6be7be4","datavalue":{"value":{"entity-type":"item","numeric-id":4079605,"id":"Q4079605"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$E5FF6A3B-4652-4F91-9150-13B8D0EEDF02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"448e5abb05ec0c10b64746c80e216ef9d23df3a7","datavalue":{"value":{"entity-type":"item","numeric-id":5674430,"id":"Q5674430"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$462876E8-7DEB-4FE3-9D56-9CF7B5C8F167","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ca4f823ca2e82e86e612699cdb65f38c133999d","datavalue":{"value":{"entity-type":"item","numeric-id":4052071,"id":"Q4052071"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$D046EC47-32D9-468C-9144-686A3EA82B33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f3bc6dfc633db1b802a1487f9064ea79563c34bf","datavalue":{"value":{"entity-type":"item","numeric-id":4046035,"id":"Q4046035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$508E32D3-C92B-4C4D-A717-A258A43B87BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cca8ae3740fcfb5a7e9f346758fcdd72ac5497a7","datavalue":{"value":{"entity-type":"item","numeric-id":4082296,"id":"Q4082296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$0749106A-077B-45CE-9430-47346F78DA9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dfc1e42883144705fb7eb08ad5b04cd023c2372c","datavalue":{"value":{"entity-type":"item","numeric-id":1163534,"id":"Q1163534"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$35F51F4F-4B9A-4DC9-96B3-256152809125","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cc8abb92210655a5bd4143cbbadd6eadb52d635","datavalue":{"value":{"entity-type":"item","numeric-id":1801222,"id":"Q1801222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$7AA05D0F-C975-41F3-9D03-D4D1525C228D","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":"Q945055$7EF1CB76-F348-4534-9FB5-08B9EF48A42C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d94c553b83f0a7713e740de3f15b3f82b8fef527","datavalue":{"value":{"entity-type":"item","numeric-id":1115858,"id":"Q1115858"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$DDBC235D-1812-4A07-9BE1-675FBEDBD04D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"901ba45472e1a0a3be8b2e40215973355027ef09","datavalue":{"value":{"entity-type":"item","numeric-id":2949209,"id":"Q2949209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$85523102-0EE2-4CE8-B121-44EE101A0812","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6496304f13783e82d12a275120aa4626825ea47b","datavalue":{"value":{"entity-type":"item","numeric-id":4231030,"id":"Q4231030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$C24EE2E2-7AFC-4257-9D95-5B650F2A7D44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cc90df82b5f45206962c7c11912a517a5a8f1843","datavalue":{"value":{"entity-type":"item","numeric-id":2848058,"id":"Q2848058"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$DA94B7FB-45CF-49D1-89B5-52DB752EBF64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f33ee1e9bddd5e600f5b1d8c8cfae347a7631b92","datavalue":{"value":{"entity-type":"item","numeric-id":3140556,"id":"Q3140556"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$2ED530D5-48B2-4A7B-9FA5-FDC114CB51F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c2d7eb80623384f2b0bdeac1b53d4423d7a886cc","datavalue":{"value":{"entity-type":"item","numeric-id":3613409,"id":"Q3613409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$FD1F472B-B274-455D-8FA6-DA87B93D1A99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d43a848f856e7add83e6907744bb466bc863e38a","datavalue":{"value":{"entity-type":"item","numeric-id":5394621,"id":"Q5394621"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$2D6E5642-2071-4ABC-B4A1-9656C23A08BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4c2c1fbb42c40132bcde18b08b5d5cb2763f5bb7","datavalue":{"value":{"entity-type":"item","numeric-id":5760872,"id":"Q5760872"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$77B6CB0D-8B5D-4B90-ACAA-C02B183813A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$C3CED198-D6FD-464C-91AC-3321F97BDEF4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f08bd5fb54cbe9466085bc1ecb3546bcc5e1f9f","datavalue":{"value":{"entity-type":"item","numeric-id":3559760,"id":"Q3559760"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$EECA927A-E0C8-4140-A262-6659C1842794","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"59a48e599820b25292d5ee25056fbb9acec2899d","datavalue":{"value":{"entity-type":"item","numeric-id":4063432,"id":"Q4063432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$58924E31-1722-4721-88DB-C4EFE78F8175","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"777f1902a1127b94884ae1ddc89768860f054a6e","datavalue":{"value":{"entity-type":"item","numeric-id":3789060,"id":"Q3789060"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$51A2CB55-F038-4D62-879C-5A4F7F3DB374","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"27124d54cb51e845e43d7ecd27812d025e0950ff","datavalue":{"value":{"entity-type":"item","numeric-id":5402572,"id":"Q5402572"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$A85970F8-B63A-4617-B26C-FCAF372CDBAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bbefacb8c8f33b0f1be9db7004061a91697d97bd","datavalue":{"value":{"entity-type":"item","numeric-id":3340842,"id":"Q3340842"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$54C6DF4B-EC92-48BB-AF4B-F7134FA2AB94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8be9375a315209f41df1b38374a5e7e956d28bf","datavalue":{"value":{"entity-type":"item","numeric-id":5807665,"id":"Q5807665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$9074D7D3-D126-46D6-B999-354676EB3E15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e7cfea5fcebfb4162710425692e427cbf2157a8f","datavalue":{"value":{"entity-type":"item","numeric-id":1103602,"id":"Q1103602"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$CED57E05-F3EB-4EB2-A790-44A854782AB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c73915bcd97bc7bb9ece7f65069678107a79a338","datavalue":{"value":{"entity-type":"item","numeric-id":753494,"id":"Q753494"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$E1FC007A-C0CD-4D28-9E2B-393CBACFE806","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eef87c90b25e8091918151481848c197b18b9425","datavalue":{"value":{"entity-type":"item","numeric-id":4226937,"id":"Q4226937"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q945055$D80B352C-F049-4D5E-AFDF-9390B86E0BB3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9564041d3b40a9ebef61749484eecf536d171f33","datavalue":{"value":"10.1007/S10817-008-9101-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q945055$501C1585-CC40-431D-AA56-8F1C26B28D09","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dbd7b8bb72e0c80f6e372a8a89999c6bac81cba3","datavalue":{"value":{"entity-type":"item","numeric-id":5387851,"id":"Q5387851"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"188e55335592ffe0a715ff84f7034070e9df4caa","datavalue":{"value":{"amount":"+0.8666335344314575","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":"Q945055$21BA81E5-4D22-43C8-9492-245F05BC643E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4826a9ebcee41c22e639fb6a714a4c993eaa4703","datavalue":{"value":{"entity-type":"item","numeric-id":707743,"id":"Q707743"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8c0001c6d86fc68baf7379593b807d05b6bf321e","datavalue":{"value":{"amount":"+0.8238200545310974","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":"Q945055$40118483-925D-4459-B3BE-11D7314B4DAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1488344e517f490998946113a8b27a39e41b9289","datavalue":{"value":{"entity-type":"item","numeric-id":5505558,"id":"Q5505558"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0973701fd1c65d055e83e3ffaeb0224c85b0dfd7","datavalue":{"value":{"amount":"+0.8194403648376465","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":"Q945055$E97CA8EC-6E9E-42DE-A79F-5081E3C8A7C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b19f108f54644f0ec26605a1f87cb8a667d4c8a5","datavalue":{"value":{"entity-type":"item","numeric-id":3541684,"id":"Q3541684"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9ea81bbda30e7cdedee0cc5c383166b8644af5fe","datavalue":{"value":{"amount":"+0.7967633008956909","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":"Q945055$0A6F1076-FEDC-4643-8F77-D3177554F0BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e276227318e6725fab8632c8a3a0db57cfb2367a","datavalue":{"value":{"entity-type":"item","numeric-id":5505503,"id":"Q5505503"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"62e4a148bbbddfa07647ab85f80d5f366475a5b3","datavalue":{"value":{"amount":"+0.7862907648086548","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":"Q945055$AE4C32AE-A363-4F76-94E2-F500B6286058","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Proof synthesis and reflection for linear arithmetic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Proof_synthesis_and_reflection_for_linear_arithmetic"}}}}}