{"entities":{"Q3192188":{"pageid":3202896,"ns":120,"title":"Item:Q3192188","lastrevid":45644446,"modified":"2025-12-11T20:20:28Z","type":"item","id":"Q3192188","labels":{"en":{"language":"en","value":"Computing All Implied Equalities via SMT-Based Partition Refinement"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6348234"}},"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":"Q3192188$3C2862AF-342D-48DD-85D4-5363485BFB2E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"79714b0b6e202146afc69770d799a12e09974b0c","datavalue":{"value":{"text":"Computing All Implied Equalities via SMT-Based Partition Refinement","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3192188$A6F204BE-8A77-4D40-A618-4EB2529DA9F3","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a02eb838027aa7ad66dcfac52ea35eb029d6cf96","datavalue":{"value":"1423.68408","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3192188$6E16FC24-BF67-48A2-96DE-FFFC2F2BD57B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"fed93b345bbfa75bc9422112a601d64a357ddc79","datavalue":{"value":"10.1007/978-3-319-08587-6_12","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3192188$1E6568EA-825B-4717-9940-9C35E2213F7B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b4e56a36e4bde76c0ca7e5e91f617c37b6d9345f","datavalue":{"value":{"entity-type":"item","numeric-id":1870490,"id":"Q1870490"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3192188$7DAEA018-3764-4D99-861B-68D21183439B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3f1a755ad39b856fc5a2e4101b7c12f7b83c7256","datavalue":{"value":{"entity-type":"item","numeric-id":483050,"id":"Q483050"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3192188$F7D3CEBD-CC54-4165-BA2D-4BBD0DB3546A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3085facee3457e7f15d7356906b0165b8709b141","datavalue":{"value":{"entity-type":"item","numeric-id":2817907,"id":"Q2817907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3192188$E0956472-5BA4-4BBC-A352-6ABF9949E2FB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7a6fb9003a97bbc70eb568e233ee4457edf484fd","datavalue":{"value":{"time":"+2014-09-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3192188$6DA01FA9-C90D-497A-80CB-A53816D5FC8B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3192188$22B1EE06-29C3-44A2-B862-DC6690151460","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3192188$E13E4C3F-D303-4A7E-8380-C3D43992F63B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3192188$34EF3219-D40B-4C65-AABA-BF61BA119FBA","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"380b70549626c4ef3b7b7381d0af432c9bd91a9f","datavalue":{"value":"6348234","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3192188$8C6FD025-45C3-49CB-82E0-0F97CE9CDFE1","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"40b8bc22e122e7aa1628742001cc8c59b8dc19cb","datavalue":{"value":"implied equalities","type":"string"},"datatype":"string"},"type":"statement","id":"Q3192188$7A2E745B-48D2-44EF-8A3C-3C12EC8B837C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bd9e4bd8f264571f02228d752cfd876f0093e7c0","datavalue":{"value":"consequence finding","type":"string"},"datatype":"string"},"type":"statement","id":"Q3192188$1F8E88A5-5D78-489E-B6A7-B9B2DA90B4BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1254a7c01d2970b87da2854c1fde40c268a1f55d","datavalue":{"value":"satisfiability modulo theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q3192188$8D4B2A23-D238-4251-AC9C-618BD0786199","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dfd2ae52b3325778b0c72742b08c947a3c4a2c65","datavalue":{"value":"decision procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q3192188$26AEE31F-6983-4D6E-A5B5-BAFDCB8D235C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"85f840ce5119480b895ac664a10de6f0a19316ae","datavalue":{"value":"congruence closure","type":"string"},"datatype":"string"},"type":"statement","id":"Q3192188$18C2FFAC-F810-45DD-AE36-083A26540097","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6ff93fcab863d9a2d7b61f398ca8507531735efa","datavalue":{"value":"software verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q3192188$FF8135C3-F573-4BA8-BA07-551854B64E02","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":"Q3192188$62FF96F7-4B09-4972-BB0A-2694D9D4F15C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"38ba5f19ea700ad6ddc03fd93e227378628d33da","datavalue":{"value":"https://doi.org/10.1007/978-3-319-08587-6_12","type":"string"},"datatype":"url"},"type":"statement","id":"Q3192188$1B5A4855-4609-4958-8F6B-4D567EF151FD","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0c318b8a02684bc4fb783d8c334d7be5f31e743b","datavalue":{"value":"W97129115","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3192188$8943CB32-8A5B-4B0C-A8FC-47AA40C42F41","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eeb8480b79c21fbc9843ec0a6188f443652e2bf2","datavalue":{"value":{"entity-type":"item","numeric-id":3460542,"id":"Q3460542"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b52aa58669e068ef47dc6182ae7ff94b4f570aa7","datavalue":{"value":{"amount":"+0.8407563","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3192188$343F2940-0C6A-4B1B-AFE6-9E0D760974B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"909541a349ce169f9b5091df34f4a238ccb451fa","datavalue":{"value":{"entity-type":"item","numeric-id":2643080,"id":"Q2643080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"99a4d0d2689066c365483dbde7e6dd89b7f05c39","datavalue":{"value":{"amount":"+0.83644027","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3192188$05A683D8-2471-4ECE-BD30-9E35A69836F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6b54ec3d11a4b8a63a3fb62a11dfd85164a29f52","datavalue":{"value":{"entity-type":"item","numeric-id":2751362,"id":"Q2751362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f9db2b16a6be0cb2acddaf16b7c3e91f17fb08b6","datavalue":{"value":{"amount":"+0.8362976","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3192188$45B340B8-C6FB-4E9A-B6D3-56E9CB5850CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4564dcbe209d24a2f509e63518773f769d6b6c9e","datavalue":{"value":{"entity-type":"item","numeric-id":4524792,"id":"Q4524792"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9688c9017a217adb6eba84ef069c613f4d20483a","datavalue":{"value":{"amount":"+0.83209467","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3192188$E6CB6546-3492-4083-BD11-56022A6B3264","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e83799d172caac9de556d975c6e02093382a2446","datavalue":{"value":{"entity-type":"item","numeric-id":3677735,"id":"Q3677735"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e769164dc8d623a2211d764b6f9022ecd88e1083","datavalue":{"value":{"amount":"+0.8297968","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3192188$24837EB5-9F1C-46AE-AE47-2202790A301D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"58720908fb6e11f462a0d45eab6a887a79b486a4","datavalue":{"value":{"entity-type":"item","numeric-id":3540073,"id":"Q3540073"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"138ea32da9e2ccaceb33f7e282184d3c0f206cc1","datavalue":{"value":{"amount":"+0.82935417","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3192188$8CBC901C-69FF-4A44-ACBA-38BADCE156B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d8049f86ea2c26568ba10a8d60118f299b0d2eb7","datavalue":{"value":{"entity-type":"item","numeric-id":2351265,"id":"Q2351265"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"138ea32da9e2ccaceb33f7e282184d3c0f206cc1","datavalue":{"value":{"amount":"+0.82935417","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3192188$2AEC393D-0FC7-4FA2-9400-7ACB7DF19918","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d37075a1917e2553c5f07df3e33a3ba49fe52029","datavalue":{"value":{"entity-type":"item","numeric-id":3707362,"id":"Q3707362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"50f2b6369651d19de86879faf259faeed58f5741","datavalue":{"value":{"amount":"+0.82902473","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3192188$C0661DC4-F0D7-44A3-B3CE-80A14BD3CF45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a928bf0b1acc5483730771259287bd383a12e220","datavalue":{"value":{"entity-type":"item","numeric-id":1961448,"id":"Q1961448"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7d88b963d953d0b3888942d7e20da295a67cf65a","datavalue":{"value":{"amount":"+0.8277743","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q3192188$38B61D52-73E4-4FA9-9FFA-F0E896C0C75E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3192188","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3192188"}}}}}