{"entities":{"Q2864404":{"pageid":2875124,"ns":120,"title":"Item:Q2864404","lastrevid":51886745,"modified":"2026-01-20T11:42:39Z","type":"item","id":"Q2864404","labels":{"en":{"language":"en","value":"\\textsf{CC(X)}: semantic combination of congruence closure with solvable theories"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6236411"}},"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":"Q2864404$23D84674-293E-4F83-B163-AA095B4AC5D3","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"13a6da5d29d559e1b3cbc4584fa3d42536967cd4","datavalue":{"value":"1277.68240","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864404$C66910FF-56AE-480B-AD98-E48957C201D1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"2a9c3e977eb61b9fc5b2fcb92fe6e8ddc0a12670","datavalue":{"value":{"entity-type":"item","numeric-id":287381,"id":"Q287381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864404$22D3A6F3-6216-4C0C-8BEF-9936AB5CF031","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"55727f9f4a7efb137e6c3bf39c513ca15ab9ea55","datavalue":{"value":{"entity-type":"item","numeric-id":851140,"id":"Q851140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864404$31F4AA14-0E16-4DE4-A2CE-AF63A69B281E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2913586d3cd4e308bb98ff964967d2ad18399c39","datavalue":{"value":{"entity-type":"item","numeric-id":287382,"id":"Q287382"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864404$DDD30E22-D26B-4A1A-96C2-0EBBF848EED8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1afbfba898283b6c4e1b3f075a124909f732f804","datavalue":{"value":{"entity-type":"item","numeric-id":2864403,"id":"Q2864403"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864404$8152B43B-E427-4D85-961A-08225ADFA340","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3478ec308a15597e43cb648673c843463f4d3028","datavalue":{"value":{"entity-type":"item","numeric-id":163528,"id":"Q163528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864404$02404EC3-87CD-4F33-8E2A-F1D2F4FF1260","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"deb6cb3450bd256fc635dc32234471403070c2b7","datavalue":{"value":{"time":"+2013-12-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2864404$35F6C3AF-5311-494F-A38F-8EAED488D027","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864404$E33134DE-62D3-480B-A58D-F9536A105ED9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864404$FA63D5AC-DD25-42B0-9E74-AF3F0A9F771F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b66e5a6e384b5dc2f5da863f8f1dfb3266130c21","datavalue":{"value":"6236411","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864404$917CE864-6CB0-43D2-AC96-FD24E2ABB636","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dfd2ae52b3325778b0c72742b08c947a3c4a2c65","datavalue":{"value":"decision procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q2864404$B379C79F-55DF-4212-B9E0-66AB1B2B7528","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"67cd9f3c039733629a1bb9742678c127ac2605f7","datavalue":{"value":"equality theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2864404$F7BF6027-EA54-4C35-A98B-4914CCF71D88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"85f840ce5119480b895ac664a10de6f0a19316ae","datavalue":{"value":"congruence closure","type":"string"},"datatype":"string"},"type":"statement","id":"Q2864404$8AD8C029-5742-4995-ABD8-E9206353FE31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66824d9cf653f7dee3c76f98a8ea1aa06432fa7c","datavalue":{"value":"verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2864404$8E51FE76-7401-4E15-B10C-DA00EF225F21","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"72973e2f3c2b37eaccccd6859e905abdf48d99e4","datavalue":{"value":{"entity-type":"item","numeric-id":17040,"id":"Q17040"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864404$D2E1001C-433C-4BD9-96BA-D9CF34CC3C8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"73bf07fb0985efe0166024eb806e5cf2244671a5","datavalue":{"value":{"entity-type":"item","numeric-id":18489,"id":"Q18489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864404$242AF430-BDB6-487F-84F6-97196985E273","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f29f161a221c0bedeec97e9d4ad10664227f4777","datavalue":{"value":{"entity-type":"item","numeric-id":16290,"id":"Q16290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864404$A1F8D000-7C69-4EEE-A2F7-5076053D77DF","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":"Q2864404$C9D605DB-6E9F-41F6-8555-C05F6B2D81B8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c441966a027378631261dc90e666a49fd0763363","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2008.04.080","type":"string"},"datatype":"url"},"type":"statement","id":"Q2864404$4C951344-4B9D-464F-AECB-AC79EC12F685","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"64189d44eacc04aa03bbdf564c87fdd84f6faf51","datavalue":{"value":"W2151546473","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864404$4AD506CE-39B6-46C8-BC7B-16DBF41FF99B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae19a70a8616a64987bb08271f6f085e5255b8c5","datavalue":{"value":{"entity-type":"item","numeric-id":3908476,"id":"Q3908476"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864404$9D0D5408-7D02-4C8E-8B94-151713B10C76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"40d202b001b8ed36eaa43fbe0e48d77bab7ad85a","datavalue":{"value":{"entity-type":"item","numeric-id":4553256,"id":"Q4553256"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864404$A64F17FF-38F5-448E-BB1C-251C87FF15C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a0aa6f30c5adcb6d4e6f2acdb35a9d6b66a77f07","datavalue":{"value":{"entity-type":"item","numeric-id":2486580,"id":"Q2486580"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864404$842AFCDD-B5A9-4380-A566-436ECEE9CFCB","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":"Q2864404$65D64D3D-3B5B-4751-8A85-DAC924BF73AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"975126c2667d6964e52988e556bf8223ff836bfd","datavalue":{"value":{"entity-type":"item","numeric-id":3883564,"id":"Q3883564"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864404$174313AB-58F0-405E-9F12-CB0FB95E3667","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a09716697edb234ce77c2288fe827cd22e3a8915","datavalue":{"value":{"entity-type":"item","numeric-id":876046,"id":"Q876046"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864404$02F62BF6-5BFE-4B0B-8CB6-E82668DD46C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6262559df3842098f118ecbbb77dfbfa994753cf","datavalue":{"value":{"entity-type":"item","numeric-id":5709987,"id":"Q5709987"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864404$5E802A35-85F7-458F-AF22-AFB7B5BC221B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a7d23d752af51468669438a65727e2f56ea73491","datavalue":{"value":{"entity-type":"item","numeric-id":3766889,"id":"Q3766889"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2864404$C0261B3A-D601-4D33-8DE8-4936C9BB8472","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"371e1e7722e9b5c647d1034df487dc0618ae5a09","datavalue":{"value":"10.1016/J.ENTCS.2008.04.080","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2864404$5A12384B-8C3F-4637-BD3A-614A91347043","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2c299621ba7744e6d8e77839a7a1048ea21b0e24","datavalue":{"value":{"text":"\\textsf{CC(X)}: semantic combination of congruence closure with solvable theories","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2864404$B28C5198-FB80-4F1F-AC72-B5DAC1A5AB6E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"30337d26ba6b5d33cb4176f2a080ff9d9c543f8f","datavalue":{"value":{"entity-type":"item","numeric-id":876046,"id":"Q876046"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a296dbb950dcee5753be1167fd9424bc2e2ecf79","datavalue":{"value":{"amount":"+0.7847854495048523","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":"Q2864404$9B43C538-D591-4789-8322-D60881AEB8DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5140a9c0589b238dec733936bc8171146d47d9aa","datavalue":{"value":{"entity-type":"item","numeric-id":3303931,"id":"Q3303931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b2a00a1ef15979c041178a300504f803a1a079b0","datavalue":{"value":{"amount":"+0.7773650288581848","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":"Q2864404$854E2AD9-2159-4F30-9483-493B186BDEDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"003eb6e6a10d86419d74d48f76d4c083b7b6b731","datavalue":{"value":{"entity-type":"item","numeric-id":5703869,"id":"Q5703869"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"92905485c6ebde411c2521cc8229f76cc3557255","datavalue":{"value":{"amount":"+0.7701970934867859","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":"Q2864404$489BAA14-E28E-422C-A4E6-7CD2AC3F4F10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"533a8b77e8a99e85fa42a571379c69b8c18274f3","datavalue":{"value":{"entity-type":"item","numeric-id":1425161,"id":"Q1425161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7130576d72263393189d247535e53d45b03f4a86","datavalue":{"value":{"amount":"+0.7630943655967712","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":"Q2864404$DB5F4B4D-EA78-494C-9395-17741193C943","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ae458d13a05846f6407623a8915e85c693e478a5","datavalue":{"value":{"entity-type":"item","numeric-id":4647541,"id":"Q4647541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4b801003b85064397b2c02f73db718b4e61b0f7f","datavalue":{"value":{"amount":"+0.7543944120407104","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":"Q2864404$26027A41-DE50-4E63-8BF9-D8B644AC0482","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2864404","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2864404"}}}}}