{"entities":{"Q1037239":{"pageid":1039087,"ns":120,"title":"Item:Q1037239","lastrevid":42832528,"modified":"2025-07-14T13:34:52Z","type":"item","id":"Q1037239","labels":{"en":{"language":"en","value":"A framework for satisfiability modulo theories"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5633141"}},"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":"Q1037239$2B105359-35E3-4CE2-B217-A5AAFA61DB11","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"dec0c2b0789800461144d473c4c9b25226ff889e","datavalue":{"value":{"text":"A framework for satisfiability modulo theories","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1037239$F9713B26-B4A0-4302-A497-15E48ADFDE5B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4d13054716e72e0453799b929f06b52aff2ce1c5","datavalue":{"value":"1192.68647","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1037239$B8A17B61-B174-4525-AA7F-482B7FBA142F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"de4a775b741b129661b3807102896dab39bea660","datavalue":{"value":{"entity-type":"item","numeric-id":438554,"id":"Q438554"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037239$C4D79695-5E12-45E1-B127-E23109E6F3F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"521ea2cb6a301fe9f22d88a2561e7746fdb48379","datavalue":{"value":{"entity-type":"item","numeric-id":246145,"id":"Q246145"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037239$AAC26128-CB5E-49F2-AA4D-B47E38DB4115","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d9925518446645d219093152a820aba790417b61","datavalue":{"value":{"entity-type":"item","numeric-id":164203,"id":"Q164203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037239$9F294109-FC72-4754-9E7C-2E102E7B7A33","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7f53dd3e5b38789996a6dcf854c0199193defe23","datavalue":{"value":{"time":"+2009-11-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1037239$88ABEBFC-6190-4C51-A75A-BD0FB27BF3A6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1037239$2A10E474-0D1E-401E-9C78-3C11362C0636","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"56b33e416638b6a238389f9e160dbe93132436df","datavalue":{"value":"5633141","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1037239$A9290BE7-8219-420B-A685-9A6C5A5B3035","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"93c047fb19c5161b32c5245d5c8c28b4500157fe","datavalue":{"value":"propositional logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1037239$4DEBDAFB-B8A1-4270-AE57-EF64789A341F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b0d152e6a9af6c905fdfdb33f1c35fcddd9b7faa","datavalue":{"value":"deductive system","type":"string"},"datatype":"string"},"type":"statement","id":"Q1037239$5A4601BB-B794-4E26-B6FD-F9CC5AB0DB8C","rank":"normal"}],"P1463":[{"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":"Q1037239$147AE20A-C7C9-41C0-B4EE-1142F71F76B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f94973da57644d5293cf3c9ac6633e23f2b0fa3a","datavalue":{"value":{"entity-type":"item","numeric-id":21445,"id":"Q21445"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037239$96381035-9199-4CB5-A185-58C44B4FF01E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"68889b620f959d2410d5024f9adee923736e93c3","datavalue":{"value":{"entity-type":"item","numeric-id":16818,"id":"Q16818"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037239$C204BFE3-08BC-45E7-904B-C32881FF21EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"040a8483cf79deba3a2eb66461dcc90b466cac47","datavalue":{"value":{"entity-type":"item","numeric-id":33420,"id":"Q33420"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037239$522EF892-3EA8-41B2-BB33-10E31E76752C","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":"Q1037239$89AF82E7-40B0-482D-8AA3-E5B4EA9B7B23","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"eaeb86c14ec690c724bee0974e7ed05305962431","datavalue":{"value":"https://doi.org/10.1007/s00165-009-0105-z","type":"string"},"datatype":"url"},"type":"statement","id":"Q1037239$6BCA29DE-1107-488C-B99E-ABF5AD37678E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9f77d4c04d81737ac1b842dd9ee4b8fc40177c92","datavalue":{"value":"W2009348615","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1037239$4700CF9C-67A1-4257-BD26-C32A1B737190","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f71dd5571a3c1c99537e11b357ad1449f45692c1","datavalue":{"value":{"entity-type":"item","numeric-id":4809056,"id":"Q4809056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037239$E183DC91-8597-4C40-AA1C-64B49F10CA92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"35351ea5314252bb01a3f01d7355b45c2893b995","datavalue":{"value":{"entity-type":"item","numeric-id":861691,"id":"Q861691"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037239$BE98A850-0A28-4361-AF1D-202743AB9802","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":"Q1037239$203AF06D-4D6D-472C-9320-FDAB2A9203D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"534cfa2da099476694e6e32aa658441dc34d268c","datavalue":{"value":{"entity-type":"item","numeric-id":2754075,"id":"Q2754075"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037239$F6C90086-7B85-4F68-A83E-3236DDEF7BD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"625f6543cb45ef040d1e85336980be3f05f00677","datavalue":{"value":{"entity-type":"item","numeric-id":5900690,"id":"Q5900690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037239$ABBE8EA8-D701-4696-ACA6-2989F4BDA1FF","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":"Q1037239$165B1E4B-ED2A-4C86-8787-613EBCE30CAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da96dfa99f70c6b2b69c48b417a516b8fa851830","datavalue":{"value":{"entity-type":"item","numeric-id":5312898,"id":"Q5312898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037239$02B5CA5D-C731-43A9-A5D6-1CAF86B483E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6730ba05bbf0433a1a497a7552c55d2bc239d0bd","datavalue":{"value":{"entity-type":"item","numeric-id":5716574,"id":"Q5716574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037239$59E4391C-2070-48C0-B9BA-45DAEEA3F6AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"931c630f243330e480767be66088a5b4e2ed5e6c","datavalue":{"value":{"entity-type":"item","numeric-id":4818813,"id":"Q4818813"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037239$71AB9D06-3F59-4931-820B-69CED4F14057","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0bfd62865a78026bb5cdd8ce719227f1e763aff7","datavalue":{"value":{"entity-type":"item","numeric-id":4804919,"id":"Q4804919"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037239$EAB479BA-CF45-42D8-A7D6-36E3CD506792","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6122a690b53da78bbd661f67fb142d629fd3a5f8","datavalue":{"value":{"entity-type":"item","numeric-id":4787213,"id":"Q4787213"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037239$DA253058-519A-4B0A-AFEA-5A8C609A6932","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"43c4614861cca8cffe8c73b1eab1c760ae07859d","datavalue":{"value":{"entity-type":"item","numeric-id":4804898,"id":"Q4804898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037239$5B0B3AE3-1539-4F65-9012-3712A43CEF1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62c7b055911e0d8bf3643774d009ace3842f48bd","datavalue":{"value":{"entity-type":"item","numeric-id":4427902,"id":"Q4427902"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037239$E8BD252A-ABB7-43D4-968D-5A423220C86C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6179b8b79bf04c1f0889052f4eb2421310a30e4c","datavalue":{"value":{"entity-type":"item","numeric-id":4708927,"id":"Q4708927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1037239$E75E42E8-67D2-4110-98B8-5B41098315D1","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"74b8aa31ca59b67bcb97246e0fb2d24b16fafc34","datavalue":{"value":"10.1007/S00165-009-0105-Z","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1037239$597752B5-C22D-45FB-A52C-8D411A3750B3","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"060b299a48c3179c59c6541e6cf5829c59574c76","datavalue":{"value":{"entity-type":"item","numeric-id":5434475,"id":"Q5434475"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"31aa39997f333a99308ed030458f5ba2c9985a2e","datavalue":{"value":{"amount":"+0.98374194","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":"Q1037239$FD06CCBA-780F-43D4-846B-39627B831F51","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":"4a9f849631b5bf36e09608681513ac657c28453d","datavalue":{"value":{"amount":"+0.9656071","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":"Q1037239$3AEA9681-841F-4E09-B662-90A20E4F6EB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f10ee01b04bf937ea18106e6d39f383b6936577b","datavalue":{"value":{"entity-type":"item","numeric-id":4931590,"id":"Q4931590"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"602cea050e1119c7b3763adde540117e80946e0f","datavalue":{"value":{"amount":"+0.9605766","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":"Q1037239$1190BE82-2AB2-47E9-8540-8EB0EA72EB63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1905f739cf619ec41f7a0632698a1edc5845bebb","datavalue":{"value":{"entity-type":"item","numeric-id":5429314,"id":"Q5429314"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"815ba2185737c84da19b802990d89ae9aa44b247","datavalue":{"value":{"amount":"+0.95294523","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":"Q1037239$BD1AC597-93FD-415E-9436-21A54C4DDAB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"44a43da73541e40b8d93166832aeb92cd4bee415","datavalue":{"value":{"entity-type":"item","numeric-id":2830018,"id":"Q2830018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"52aafc50fde69e21e89b3050effe73664bde4a88","datavalue":{"value":{"amount":"+0.9472568","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":"Q1037239$EC676210-AC39-446D-8FD1-EB6D82B0226B","rank":"normal"},{"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":"fcac6db393c3c0ad388d7b61142f19fc265ac336","datavalue":{"value":{"amount":"+0.94251853","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":"Q1037239$3BEA0F48-0C0C-44BA-B408-EF7268F3AC5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"773a16eb821af62aeef0f8b676ac1158efeefebc","datavalue":{"value":{"entity-type":"item","numeric-id":3651277,"id":"Q3651277"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e7fb990c8c113f7d09ba98407361778d7ef60129","datavalue":{"value":{"amount":"+0.9424212","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":"Q1037239$90E8F2F3-70A1-48AF-9463-0B9C6152389D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2e8af80161dc8c18c8bc8a8c02cd47c9c758f8f1","datavalue":{"value":{"entity-type":"item","numeric-id":438578,"id":"Q438578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"71986eae41a96eee650b1394448b109109d98931","datavalue":{"value":{"amount":"+0.9407268","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":"Q1037239$9C93BBAA-2F87-4298-8DCD-83C56A75C77C","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":"fd93bba21569624ec315e6f598810ca462e09a01","datavalue":{"value":{"amount":"+0.9393136","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":"Q1037239$E1EE6A8B-AA3D-4072-B8F8-A3F1BE4265FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e218af8cd43ad3720c9bf48989333d3d35e67744","datavalue":{"value":{"entity-type":"item","numeric-id":5756580,"id":"Q5756580"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4232a320f818ed4a61a6dad7163649427b07a9e8","datavalue":{"value":{"amount":"+0.928352","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":"Q1037239$EC5552F5-D991-4912-9855-DA2556EDE3BE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1037239","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1037239"}}}}}