{"entities":{"Q2303254":{"pageid":2313997,"ns":120,"title":"Item:Q2303254","lastrevid":71799036,"modified":"2026-04-14T00:37:02Z","type":"item","id":"Q2303254","labels":{"en":{"language":"en","value":"Conflict-driven satisfiability for theory combination: transition system and completeness"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7176611"}},"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":"Q2303254$51695F1F-75A7-4F4A-A78A-899F08772AD5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"200180e3f0dce6f3ddedccf8a10d450aa0911e4b","datavalue":{"value":{"text":"Conflict-driven satisfiability for theory combination: transition system and completeness","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2303254$0199E6C1-06C5-42E7-A20D-A8BBFDD38484","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4df0e6addf8f3368567b02b22a1abe5ca8e72a92","datavalue":{"value":"1468.68194","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2303254$B1414536-5AF9-4C76-8EB5-F5CA8EDE2A95","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b455290f5b835c3773a6eb2262897ac70e7a163b","datavalue":{"value":{"entity-type":"item","numeric-id":287273,"id":"Q287273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303254$F08F43BF-CBA6-4171-94DD-FF3D93E724A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a6be8d909a46685b6a24cecd253b3dd33cd2a6cb","datavalue":{"value":{"entity-type":"item","numeric-id":832718,"id":"Q832718"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303254$FF9636E5-B114-4A52-AB59-B647CF8FCE53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8f977cc4afe30a7452131df7ff084411daffbbaa","datavalue":{"value":{"entity-type":"item","numeric-id":532428,"id":"Q532428"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303254$990E5831-F149-4D71-ADC2-4F2C65F3511A","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":"Q2303254$A87AB5F0-C203-48C2-825B-264736411B7A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"61e2e5951dfff50ebb9b8606073c3ef7da57bd09","datavalue":{"value":{"time":"+2020-03-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2303254$1C0CB633-C00E-41C9-A402-5DB882F2F67B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2303254$EE641597-2146-46EC-85C6-C6DFA04E2AEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2303254$A8B20158-3524-4966-9513-7E2746DA74D1","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6905fe22fe20bead63cc92b8dde65799ae0947df","datavalue":{"value":"7176611","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2303254$ED4AFA7F-59C1-4E1A-A0C6-828C67C34F8F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6c97c87aad358aaa4a159991a487a984d3a19cc4","datavalue":{"value":"theory combination","type":"string"},"datatype":"string"},"type":"statement","id":"Q2303254$FEF3FED3-5A14-4719-AE12-05B3F22D0D1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ba541055dc9223ac28a9cc043149f1fd4c5baf5e","datavalue":{"value":"conflict-driven decision procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q2303254$4112A271-CC21-40DD-9756-2BDC9C9276B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b0133bb82e5a2899974ef5a92a207f1239299d2","datavalue":{"value":"model building","type":"string"},"datatype":"string"},"type":"statement","id":"Q2303254$E693B1DF-472F-4D8E-99B3-86C430022688","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4b395e8f6acd180e1625664cf0f73ca38f664e9d","datavalue":{"value":"satisfiability modulo assignment","type":"string"},"datatype":"string"},"type":"statement","id":"Q2303254$94029414-3F58-4AFC-A71E-75A26D153C1D","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"85575b60ef4d0a8413d3c895be2530b8915bc3fb","datavalue":{"value":{"entity-type":"item","numeric-id":16612,"id":"Q16612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303254$402D0D5C-8192-453E-9DD5-A065A3CFD029","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":"Q2303254$4CBF4B87-7602-4249-8B29-5A32AD98808F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b23c7f364b8e7efc46e48b6a5c70d3100f19d020","datavalue":{"value":"https://doi.org/10.1007/s10817-018-09510-y","type":"string"},"datatype":"url"},"type":"statement","id":"Q2303254$7514FA24-70D3-44BE-A243-8EE3FF9AEA21","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"dfb81066a75c23c277326d335c760b8cb776452c","datavalue":{"value":"W2907207368","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2303254$58830974-6991-4FBD-BD23-ADDD33C94C06","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"9c10bd59885420c4841d56d098f27b4158c1d680","datavalue":{"value":{"entity-type":"item","numeric-id":4737130,"id":"Q4737130"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303254$158B5CB9-E1B3-42AD-9390-CBE9D85ED771","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"14bd97e9dec390545916db4e89e737371beca26b","datavalue":{"value":{"entity-type":"item","numeric-id":5387916,"id":"Q5387916"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303254$A0085275-0764-42BD-B289-12A6328FCB6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f942974cb95506daf6c9f8a39d7c2f272d4faa3d","datavalue":{"value":{"entity-type":"item","numeric-id":2405239,"id":"Q2405239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303254$E0FBFA49-2509-4B24-AAF0-5AFE140F3DA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"64edbd4b0368a46cc24983dcdc802e4982142495","datavalue":{"value":{"entity-type":"item","numeric-id":5310200,"id":"Q5310200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303254$20CF7818-FFB7-4D14-BBEE-7A0A8C32BA15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5d4d5df30bde2099983c3bf5f07484cf1031c989","datavalue":{"value":{"entity-type":"item","numeric-id":3181652,"id":"Q3181652"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303254$91DC9D29-387B-4554-A307-088148FD9874","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ddeddf292e13fd796c5c20e153357856b636f89","datavalue":{"value":{"entity-type":"item","numeric-id":2926635,"id":"Q2926635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303254$42809049-628F-49EE-94AF-18F3B3911CD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6fa4c2387ad30aeefcdaa752dcaca22072d33adf","datavalue":{"value":{"entity-type":"item","numeric-id":2961575,"id":"Q2961575"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303254$48541A75-9F81-49F6-9DBE-3D2EC16DA470","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0935562160404eb7beee2a862bd06bed764fe33","datavalue":{"value":{"entity-type":"item","numeric-id":3172894,"id":"Q3172894"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303254$FC354740-6CFB-4BA9-8B64-571E2BF221BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d6ef9008a9fa143fe20e12a5c9881d6597928911","datavalue":{"value":{"entity-type":"item","numeric-id":5200035,"id":"Q5200035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303254$92BE4DE3-1591-4452-AAFC-A9064DD8F9F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d77121ca06023666fb3b31fe1611bc7b34ff56df","datavalue":{"value":{"entity-type":"item","numeric-id":2908506,"id":"Q2908506"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303254$8976F407-C466-48D8-B709-FA6D2B8F3702","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e4e6adf13c6408e6c2eebe9bb0eee05dbe30b987","datavalue":{"value":{"entity-type":"item","numeric-id":3524998,"id":"Q3524998"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303254$31C2802B-AE73-4253-968B-516415C8D381","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f814032017aa40390d4c6f26a550d62bb08ff374","datavalue":{"value":{"entity-type":"item","numeric-id":5503674,"id":"Q5503674"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303254$68E424B5-A71D-4B15-BA82-3968EFB7AC4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce7b2dd2863358cf2a528999ec6b006fdf400b99","datavalue":{"value":{"entity-type":"item","numeric-id":3899468,"id":"Q3899468"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303254$566CDCB3-5BCA-4E48-B53C-D00DBCBBBB18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79db93a0bb311f56c816d6ffc92dd7b60e23250d","datavalue":{"value":{"entity-type":"item","numeric-id":3455223,"id":"Q3455223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303254$E6B1D0E5-6993-40D9-BF41-2162EE73C713","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a3d8be39100c65d1e448187a4dbf9fe46245230","datavalue":{"value":{"entity-type":"item","numeric-id":2818018,"id":"Q2818018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303254$A1432C9F-6F2D-49B5-9BA1-1D569376FD8D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3be9b5ee24bd9dc111b6b1987d56d8645379fa49","datavalue":{"value":"10.1007/S10817-018-09510-Y","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2303254$1BBED257-E016-4F8D-97D0-A323F5DEED60","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fb29bdfd2432d520a44e436c9a9d449e487108e7","datavalue":{"value":{"entity-type":"item","numeric-id":2405239,"id":"Q2405239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7d0311a77f716b766515fe4c92bec20f3a0357f3","datavalue":{"value":{"amount":"+0.8881899118423462","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":"Q2303254$AF8B19BB-63E2-4693-B8BB-A32DE7837E4D","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":"6e75456e5bd8689a8a9c3f2ba532bfc10726a879","datavalue":{"value":{"amount":"+0.8164408206939697","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":"Q2303254$22CF3DF2-F598-436A-BD90-2F03EB855415","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c3e71bfb5b68d2283442ce2c6ed865faa5ef3fdb","datavalue":{"value":{"entity-type":"item","numeric-id":5756564,"id":"Q5756564"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"966ec15eada10c30fadf35b929f70183073eb6e6","datavalue":{"value":{"amount":"+0.781502902507782","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":"Q2303254$CCB626C3-9364-443F-B29D-30C3A10B2CE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"18ba98873d052f5816175646d512a17079b79c03","datavalue":{"value":{"entity-type":"item","numeric-id":3176369,"id":"Q3176369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"48c71cb83663f8f94dfa1a4745fa09bd5645be3e","datavalue":{"value":{"amount":"+0.766120970249176","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":"Q2303254$01C38FD6-15A6-4F76-9809-AB0353183A4F","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":"4717527eb8bfb2c15e60628963c8031cc7cca57a","datavalue":{"value":{"amount":"+0.7646557092666626","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":"Q2303254$A25B0218-73CC-4346-9E60-EDEE09A71124","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Conflict-driven satisfiability for theory combination: transition system and completeness","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Conflict-driven_satisfiability_for_theory_combination:_transition_system_and_completeness"}}}}}