{"entities":{"Q2375732":{"pageid":2386475,"ns":120,"title":"Item:Q2375732","lastrevid":56683302,"modified":"2026-03-18T19:13:13Z","type":"item","id":"Q2375732","labels":{"en":{"language":"en","value":"A unified framework for DPLL(T) + certificates"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6175991"}},"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":"Q2375732$FEC91C49-F0BF-47B6-983C-7F886BCE47BE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"99db9895e7977446466ff490142a16f9d3cd6d37","datavalue":{"value":{"text":"A unified framework for DPLL(T) + certificates","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2375732$E31EBFF6-75E9-4256-AB7A-5522C929FA5A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"eb410ba2d415138b1e4feaec8b71200a675b72e1","datavalue":{"value":"1267.68146","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2375732$D1F9960D-38C9-4315-A1F2-A809DBEC8D42","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a2df3647535a5d177a9346b21c981a8135e9d38f","datavalue":{"value":"10.1155/2013/964682","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2375732$35F9DD41-1DCA-4144-AA03-9FB8497A2EF4","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"25f90f689538369c96cf81116800716356f3e202","datavalue":{"value":{"entity-type":"item","numeric-id":289971,"id":"Q289971"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375732$7B974711-A676-40AA-90F2-FD48AAEC5E0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"34a2e3a849f7afbd44d878457dc05f4cc4bbe211","datavalue":{"value":{"entity-type":"item","numeric-id":270244,"id":"Q270244"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375732$FC145829-6446-4F90-9EAD-E3029B100591","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"19c17cf4b757376e81bb18052c33891da6bf831a","datavalue":{"value":{"entity-type":"item","numeric-id":832259,"id":"Q832259"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375732$7B175B70-CFAA-4F2E-84D2-7963A9E74A5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3627b82cbdcf824882c2564acab074471f4e73a9","datavalue":{"value":{"entity-type":"item","numeric-id":372855,"id":"Q372855"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375732$9641CB55-1B83-4F5D-B7EC-8FDDB9BA2CB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"547768faf13f2f7e708d264c604987298599ca03","datavalue":{"value":{"entity-type":"item","numeric-id":625278,"id":"Q625278"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375732$4B399315-F3C4-42C5-9FAB-AC5E1DC3A72C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"bb299feb2b87699ac8beef494c52fd2765eaf609","datavalue":{"value":{"entity-type":"item","numeric-id":118601,"id":"Q118601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375732$BCF11721-747D-47E0-BEA3-4E2A1E69C496","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b84d2a34981f1c1a0d0fb543ea5aabc14a21194b","datavalue":{"value":{"time":"+2013-06-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2375732$ACB0FC4D-00EA-4638-9F71-F52A3492530E","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"f9d150154d59662ad2b6baf52ece62ad1c30b53b","datavalue":{"value":"Summary: Satisfiability modulo theories (SMT) techniques are widely used nowadays. SMT solvers are typically used as verification backends. When an SMT solver is invoked, it is quite important to ensure the correctness of its results. To address this problem, we propose a unified certificate framework based on DPLL(T), including a uniform certificate format, a unified certificate generation procedure, and a unified certificate checking procedure. The certificate format is shown to be simple, clean, and extensible to different background theories. The certificate generation procedure is well adapted to most DPLL(T)-based SMT solvers. The soundness and completeness for DPLL(T) + certificates were established. The certificate checking procedure is straightforward and efficient. Experimental results show that the overhead for certificates generation is only 10\\%, which outperforms other methods, and the certificate checking procedure is quite time saving.","type":"string"},"datatype":"string"},"type":"statement","id":"Q2375732$72579683-B8FD-40AC-ACF4-797EA9715F1B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2375732$F34F067D-AA8D-4B16-82C0-481635A4DC7D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2375732$B40341AC-AFED-4B51-9CD3-0E45D51C362E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"de0b635c44fb509d2390d4208c147521d2570189","datavalue":{"value":"6175991","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2375732$CCD0B07E-7D39-45A1-8A6A-9ED3549D64B7","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ac8daf9b2a0058692665d0c45ec7b53d7ff6b82e","datavalue":{"value":"satisfiability modulo theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2375732$E16E1375-883A-45F6-9EA6-F3657F71FE67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"61439d791f6aac729372268f16b553bcf47e3b78","datavalue":{"value":"SMT solvers","type":"string"},"datatype":"string"},"type":"statement","id":"Q2375732$52DEE4CC-60BF-4E88-AA66-AF632F9EB28F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cdfac48fd034399c77d348480e75efcf63067c46","datavalue":{"value":"DPLL(T)","type":"string"},"datatype":"string"},"type":"statement","id":"Q2375732$82644B46-6FCA-4FA2-BEDD-2F19A5CF68E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"da572233d864212611d32c40a69f00035f36fa4e","datavalue":{"value":"certificate format","type":"string"},"datatype":"string"},"type":"statement","id":"Q2375732$567B638F-7132-4A96-97F6-64D6541B73DE","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"746368ad21583ab2290fca59b50c6d9b461c66d8","datavalue":{"value":"Q59007217","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2375732$E3898C73-4518-4873-8833-3BBB8668882E","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375732$FD11C152-8A28-463D-996F-85F1162BB1CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3ac1e8c13c0130a75f4cf78841def0133e1a8ff4","datavalue":{"value":{"entity-type":"item","numeric-id":20425,"id":"Q20425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375732$778ADA4D-2682-4381-9A08-9E25DF116D5D","rank":"normal"},{"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":"Q2375732$B50ADECB-FCCB-4BB8-BBF1-DC1447B379AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6d1b503d7c8f19634e207574177819c306621855","datavalue":{"value":{"entity-type":"item","numeric-id":17038,"id":"Q17038"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375732$35F61B80-2F82-4E91-9086-4E81ED7B1E1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"478f9061f14e098e3fdf3fe3667d3a7084c42e61","datavalue":{"value":{"entity-type":"item","numeric-id":18982,"id":"Q18982"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375732$BF1C9549-83AD-4A42-BD3D-E8F06685A766","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8449db7d9aaa28101ba7b0de8e98d9c446365070","datavalue":{"value":{"entity-type":"item","numeric-id":13332,"id":"Q13332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375732$94170D2F-8BC6-4D05-93DD-02E57C361D9C","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":"Q2375732$17A4E733-F0B7-443C-A641-B53698912D99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"60c977c73f66c80db6a0782a3e55d401ee00ddc1","datavalue":{"value":{"entity-type":"item","numeric-id":19150,"id":"Q19150"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375732$35037487-7405-4C08-9F9F-E6175ADEB6E3","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":"Q2375732$DAF17713-CF13-4B99-B2D4-EAD68DDBC21F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fc5e8f5d2d35dfee91c63548d1e15c88bb9ed23e","datavalue":{"value":"https://doi.org/10.1155/2013/964682","type":"string"},"datatype":"url"},"type":"statement","id":"Q2375732$92FC2BAE-78F8-4058-A33F-29EBEE7EC924","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c4167b4c92a30b1001a0f470155cce451447a8bd","datavalue":{"value":"W1517540595","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2375732$311FE0B6-5162-47A2-9378-B6D9787A9205","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"652707f3c517fc0bc45fb7ef7e533228515c0c0d","datavalue":{"value":{"entity-type":"item","numeric-id":5715680,"id":"Q5715680"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375732$544946E7-23D6-45DC-A7C3-C21E4448AE7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4f0d636879b192f180d0014cf8561701adfc310","datavalue":{"value":{"entity-type":"item","numeric-id":1861908,"id":"Q1861908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375732$F53C5680-7DCF-4BE0-8E60-173311BFA44B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0086f5e874fe7e4f38ea6905507c6d71ae7ad220","datavalue":{"value":{"entity-type":"item","numeric-id":4399249,"id":"Q4399249"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375732$7A0B5AE9-CA0B-4A88-B5F9-A1575257EBDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b7948d2ae997be513a92df2486b836c4e1eaa12","datavalue":{"value":{"entity-type":"item","numeric-id":5667480,"id":"Q5667480"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375732$B528683F-5BCE-4FC6-85DB-AD00BFB90492","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62cff4d07ffcb71b5bb9f399ad2347b51931f095","datavalue":{"value":{"entity-type":"item","numeric-id":5621961,"id":"Q5621961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375732$9FFEC8AD-687B-4472-8999-9E40185A91B2","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":"Q2375732$91A6FF2D-092D-4891-90B0-BAB1D15B2423","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9370899dedc1d653d16f1f5aaa8b6c6be96f529c","datavalue":{"value":{"entity-type":"item","numeric-id":3604000,"id":"Q3604000"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375732$9A4D51C1-BF8C-48BD-BD7A-14EEB433056A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dee09e75a430fc0be911c9a36f98899b21bf0296","datavalue":{"value":{"entity-type":"item","numeric-id":2441776,"id":"Q2441776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375732$D5351B66-A839-4301-9B6D-D53F9311BEF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d2b783d0052b7f250a9573410e9be2b4624ef11e","datavalue":{"value":{"entity-type":"item","numeric-id":5899057,"id":"Q5899057"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375732$8BB50BC0-4A2E-4FE4-8A73-DCFB6EFF2963","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b00f83e613d735519b98c96b09a9cf48e50fb9d0","datavalue":{"value":{"entity-type":"item","numeric-id":3612475,"id":"Q3612475"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375732$EF4E742E-E5B9-4573-B808-BEE101B8056E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c22bde11e78369a6138771e56f2c61a2713ba27a","datavalue":{"value":{"entity-type":"item","numeric-id":5458346,"id":"Q5458346"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2375732$1BEB7934-0DA2-447B-9BD6-9F0BF375B019","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e6e92bb1e52dcbe4b71fbb4fb8a9dabdf590a402","datavalue":{"value":{"entity-type":"item","numeric-id":5920089,"id":"Q5920089"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"69460d0b96d85b1dc548bbc5b6fe2b02976758fe","datavalue":{"value":{"amount":"+0.7739749550819397","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":"Q2375732$A884BDC4-1A35-49BE-AF54-3B8098A6E70B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3e53b32fbbe403880914d5edbf7f5343988e28a4","datavalue":{"value":{"entity-type":"item","numeric-id":5919480,"id":"Q5919480"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e69be3cbf1558e3ed3b23ec5ba9686b34188b475","datavalue":{"value":{"amount":"+0.7733708620071411","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":"Q2375732$866FF209-9D60-4B02-BB31-E09A2E9162FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1dc4a898c2ce53e9d3b4432ba9d09cae8e716f24","datavalue":{"value":{"entity-type":"item","numeric-id":2441776,"id":"Q2441776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"608a9ff6bc6f91ede4e0889db1044c44a7ecb4f4","datavalue":{"value":{"amount":"+0.7505236268043518","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":"Q2375732$0D0CC962-9527-4DBC-92D6-40A27C831DF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b25840e9689e28a5767a31e8370e4b859c5091dc","datavalue":{"value":{"entity-type":"item","numeric-id":5458346,"id":"Q5458346"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a4a169e05419343e44529586626820fe98dfbc96","datavalue":{"value":{"amount":"+0.7476369142532349","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":"Q2375732$509F5CF7-3B67-4117-8C7C-3E99DB449E82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cbd1f875057910272dc1f6cefa7437b5d6cd54c8","datavalue":{"value":{"entity-type":"item","numeric-id":3455223,"id":"Q3455223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0eb97e8cca3df2107bd4fea5383eb5d9dc9802ab","datavalue":{"value":{"amount":"+0.7398782968521118","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":"Q2375732$47E4426F-B655-4963-81DA-B9A881C9D04F","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":"Q2375732$C597D837-3BF3-45C0-9605-D0E30530912C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2375732","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2375732"}}}}}