{"entities":{"Q3084983":{"pageid":3095698,"ns":120,"title":"Item:Q3084983","lastrevid":51214982,"modified":"2026-01-17T07:00:03Z","type":"item","id":"Q3084983","labels":{"en":{"language":"en","value":"Combining satisfiability procedures for unions of theories with a shared counting operator"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5870672"}},"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":"Q3084983$532003A0-61AC-4E6C-89D0-85497142E898","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"829a822ca58e94ae211e04c07cbec77e7c9f5fdc","datavalue":{"value":{"text":"Combining Satisfiability Procedures for Unions of Theories with a Shared Counting Operator","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3084983$C366ED2E-31F2-4715-924C-6918353B2CF6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"dfa6fc37e86e23d3617235ae9a9195fbdd3aaf15","datavalue":{"value":"1215.03051","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3084983$E5687A46-D644-4E61-B82D-202119E08618","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"59decd6d87c6f21753961b8cab79c21904988ce6","datavalue":{"value":"10.3233/FI-2010-362","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3084983$D44157BE-9462-4AE4-BA4B-0DC8378DA1D1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"50e50528f45a8bb28ce09efe5389b579bf5ff46d","datavalue":{"value":{"entity-type":"item","numeric-id":438571,"id":"Q438571"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3084983$7763602A-4EE5-484F-86A1-62BEC7E10149","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"28d2abcbf491e57c8b4eebf23b3e8446f4e5bbb9","datavalue":{"value":{"entity-type":"item","numeric-id":831918,"id":"Q831918"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3084983$DA856CBB-04CB-4E22-93B1-1083322DDC86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d5450522126073beebe5b41bdc84b794c874c239","datavalue":{"value":{"entity-type":"item","numeric-id":437030,"id":"Q437030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3084983$8ECB9409-C7AF-407A-9C17-6478474B9FC4","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"1529db038bde6a8aed76ac5e8432917aee1a9200","datavalue":{"value":{"entity-type":"item","numeric-id":2803574,"id":"Q2803574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3084983$2536827B-624F-4D03-9FC5-DA71E3892593","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"86a51260412b40e5c53c8066fdea67849229bf08","datavalue":{"value":{"time":"+2011-03-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3084983$E07F94EF-E0BC-467D-888B-7547784FF568","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3084983$BBE363B8-DBF3-4BF8-A837-E392244710AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"407654cf92f0702e03297e7fe541e25fa3f13c2d","datavalue":{"value":"03B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3084983$7507FF08-0E92-49AA-B0DE-0B1EF73533B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3084983$E75005B5-C5EC-4288-A0B1-8EF21CEC3366","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"14cf74de25853c940589b125137b792dfb2d092b","datavalue":{"value":"68P05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3084983$3FA7F63E-05F8-4C64-925A-7A010A31EC5D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a3fc4eefcfa9dbc7865c0b2acd9402518cac6703","datavalue":{"value":"5870672","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3084983$FE4033AF-8E0C-4854-88E5-32B283022A34","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d7642a179dc6398109b7aea6426b903faf23d539","datavalue":{"value":"satisfiability procedure","type":"string"},"datatype":"string"},"type":"statement","id":"Q3084983$BF4B4E9E-83DE-4C98-8163-3F88B31E1A98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ca82b8126faca2bdab3ffa77f0c22600be2e10e6","datavalue":{"value":"equational reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q3084983$360FBEC5-F6C2-4EBF-AA90-7DA56ACF357B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aec7585aa240cc9f6ae90a8fbd142bca310b3e34","datavalue":{"value":"union of non-disjoint theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q3084983$4C118615-202C-4045-BEC4-F5E38530675C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7e3d8a223a52974611f3d6eae00bf94de8f1f743","datavalue":{"value":"integer offsets","type":"string"},"datatype":"string"},"type":"statement","id":"Q3084983$77283087-A688-4707-9C4B-E093833750CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"48fe5da30f2000a910dd1a06f280ea2b3174328d","datavalue":{"value":"decidability","type":"string"},"datatype":"string"},"type":"statement","id":"Q3084983$6736FDE5-9D58-4F07-B931-02E57B1FD036","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"43d8de44b3f88bd19a871628a3509981cd748562","datavalue":{"value":"data structures","type":"string"},"datatype":"string"},"type":"statement","id":"Q3084983$B146FA37-A908-40CC-97F5-78C447605857","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1bc824dc04e7b8e37625108dfb862d4dd023ba72","datavalue":{"value":"arithmetic constraints","type":"string"},"datatype":"string"},"type":"statement","id":"Q3084983$940CBC15-EC48-4CFA-ACF1-5E66BA9EAA13","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":"Q3084983$E2283C2B-853F-47E9-BD6C-A7078FD7221F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c4c9111c8b72609843622afd2c60d69e338cf1f1","datavalue":{"value":"https://doi.org/10.3233/fi-2010-362","type":"string"},"datatype":"url"},"type":"statement","id":"Q3084983$94DF9194-B7CA-4504-A004-E8226B2664A3","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"4d979b16fa86619a7ac87f756e53dd2c46e0133b","datavalue":{"value":"W1501719149","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3084983$35CE6AB6-D58B-4494-811C-E7C6D6933D67","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a2a0c45094f5cb780e5c9a50d8a3162fa6398d9b","datavalue":{"value":{"entity-type":"item","numeric-id":3655209,"id":"Q3655209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"92bfb22f098d1146d96e8fd92c98f4612951a67a","datavalue":{"value":{"amount":"+0.8535484671592712","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":"Q3084983$82409784-461A-4D67-A933-3B69736494F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"43b31fc71a6b23556d529814a409bb49f6e92fa7","datavalue":{"value":{"entity-type":"item","numeric-id":1853591,"id":"Q1853591"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d40e7a7cb0f7f20e308cbdc221afd81ec1f0dd8a","datavalue":{"value":{"amount":"+0.8160634636878967","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":"Q3084983$6C346FAA-A081-4CF9-B6BA-63AF8B1C7B69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bedb276801d45087077262c44e87c78cdcacf6a7","datavalue":{"value":{"entity-type":"item","numeric-id":3617773,"id":"Q3617773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"33d2528c4b6a3f13b805eec4846d0235aa3f2c1f","datavalue":{"value":{"amount":"+0.8057454228401184","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":"Q3084983$A1F7E1C0-8607-4320-95A7-C95CCFC95608","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"663aa1de8a6d978e2db16aaa337bd4bfbec378db","datavalue":{"value":{"entity-type":"item","numeric-id":2185458,"id":"Q2185458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c94cf84c8fa342d7be0247b24c7407a231f8f45a","datavalue":{"value":{"amount":"+0.8006306886672974","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":"Q3084983$14D8908B-8BF0-4F49-8BB9-3F32F3A35BFC","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":"2c1c23a3070207226c377565a8383f28506ffbd5","datavalue":{"value":{"amount":"+0.7971537709236145","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":"Q3084983$5A25A650-EE40-4E58-B970-DF297BE34912","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3084983","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3084983"}}}}}