{"entities":{"Q2180230":{"pageid":2190973,"ns":120,"title":"Item:Q2180230","lastrevid":56736609,"modified":"2026-03-19T13:23:39Z","type":"item","id":"Q2180230","labels":{"en":{"language":"en","value":"Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7200363"}},"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":"Q2180230$34D6C379-3951-4C97-967C-E89396A3A1DF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"bf3f11ddc8f44f0cde146b14fa73be24e8f944c3","datavalue":{"value":{"text":"Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2180230$6F88EA7C-9DE8-4884-BC77-840187C2794C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8aaffa1bdfe508d1bc1bd11d5270f340cc42cd5b","datavalue":{"value":"1435.68362","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2180230$181A91D4-2B09-450D-8B8B-BA277C59DCCC","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c7abd363234277abd0cffe41dce072f5efea6581","datavalue":{"value":"10.1007/978-3-030-29007-8_13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2180230$FF197540-5A9D-404F-BD5C-ADB5CCA810F2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c3f2f1d2bd01a9a751768a2f79d364b7811b4ac4","datavalue":{"value":{"entity-type":"item","numeric-id":2180229,"id":"Q2180229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2180230$FE92A054-8258-47D7-9A4D-15A733351697","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b8a60aaa0b31cf201c3bd6bbf4033ad1d57b0d05","datavalue":{"value":{"entity-type":"item","numeric-id":1791158,"id":"Q1791158"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2180230$24276ECC-508C-402F-B84A-D60C5B5D5AC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c8e2771b20e3c98dace74591de69baf1cddaba7f","datavalue":{"value":{"entity-type":"item","numeric-id":515686,"id":"Q515686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2180230$81A391C4-5635-433D-8B46-B9B2912A47BE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6d0c48627b068f854a947856c3807165d49ca3ba","datavalue":{"value":{"time":"+2020-05-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2180230$50F3811E-3BA7-4421-A01E-388CFBE17387","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2180230$B197D574-C6FC-4774-A6EF-32299123EE09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7083a5d146d78edf9fc7469a5d9b0c104122f1b7","datavalue":{"value":"68R07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2180230$C69D9F6D-667D-4EFC-9B15-92C661173FF9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"07ab635a353ce95aec0c13618e506a1b25898b28","datavalue":{"value":"7200363","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2180230$A3409B39-EBF4-48DB-9D2C-7E93D33F5B40","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cdfac48fd034399c77d348480e75efcf63067c46","datavalue":{"value":"DPLL(T)","type":"string"},"datatype":"string"},"type":"statement","id":"Q2180230$47F354B2-686F-4972-818A-67ECBFC930C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e5f5af9bb3f40eb3a311a98e7815fe1ea7154ddc","datavalue":{"value":"Farkas' lemma","type":"string"},"datatype":"string"},"type":"statement","id":"Q2180230$A084AC16-4871-434E-AC5E-9137C2B37474","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b2e693c2fb316708f6e0f61d4b0ded45ae0b8b3d","datavalue":{"value":"simplex algorithm","type":"string"},"datatype":"string"},"type":"statement","id":"Q2180230$A38AF7DA-05EA-4628-974A-80C01675326D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dac36a0d5bcef050bd5c5ec480998b0eb01458a6","datavalue":{"value":"SMT solving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2180230$4FDB72D9-882E-4524-85D3-0A63CD13DFB2","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":"Q2180230$85D852C2-2288-4355-9F5B-A937BEB278B1","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":"Q2180230$1E56183C-3800-4483-AED1-5C024F1F0B04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2180230$A1EFD48D-C405-46D8-9C82-FB732D221CEE","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":"Q2180230$6B339884-8BB6-4E05-844A-37F44F737442","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"db94492dd16d7404f3295ef880bdedf8025e1824","datavalue":{"value":"https://doi.org/10.1007/978-3-030-29007-8_13","type":"string"},"datatype":"url"},"type":"statement","id":"Q2180230$48D13E38-BF45-4CA2-A551-A5FE27A5D10A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"8d57562270ea645caa12a08f311f9cf1240d4b3f","datavalue":{"value":"W2969660840","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2180230$A8AEA75E-27BD-49FB-BFB3-F45FD7AE7320","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"690b51da4d8f34f1d9ad367e3d2b1df11a514a2e","datavalue":{"value":{"entity-type":"item","numeric-id":4647860,"id":"Q4647860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"31d62f96098b6d1057e978f493f8a1451677efa4","datavalue":{"value":{"amount":"+0.7814573049545288","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":"Q2180230$785C66FD-BC05-4B97-BE9C-B50FC165916E","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":"b211b1b97e91093c88e0c842e16ee6c75bec0cf4","datavalue":{"value":{"amount":"+0.7765233516693115","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":"Q2180230$3548C9B2-2921-4169-81B0-C971265D68B5","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":"1aa1f1993a18c17eec90b4f0d4649e5fcdb6955a","datavalue":{"value":{"amount":"+0.7676292657852173","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":"Q2180230$796F248F-DC5C-4730-9946-71E380E27641","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"75cebb44bb9f7313a4886ffb381ecde6d2b331ad","datavalue":{"value":{"entity-type":"item","numeric-id":2908479,"id":"Q2908479"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"073b7ec320cd00ae2c41582c72bee207c635691d","datavalue":{"value":{"amount":"+0.7607917785644531","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":"Q2180230$5730657F-F41A-405F-B73A-D7F56BA74965","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":"8d2c6a4edcf534192d8808cf70c3ea021df434bf","datavalue":{"value":{"amount":"+0.7564879655838013","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":"Q2180230$DBF4A6FF-D503-4DF9-A555-14E233E56EC9","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":"Q2180230$24AA0BAF-9A9E-4B72-A87B-CDA46E918176","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2180230","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2180230"}}}}}