{"entities":{"Q438578":{"pageid":440345,"ns":120,"title":"Item:Q438578","lastrevid":61924770,"modified":"2026-04-11T02:35:18Z","type":"item","id":"Q438578","labels":{"en":{"language":"en","value":"An instantiation scheme for satisfiability modulo theories"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6062064"}},"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":"Q438578$E4C76416-E0E3-4E6C-9B79-FC859965EE03","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"632bca9041e50047ead2b7ae24e2ece68995115a","datavalue":{"value":{"text":"An instantiation scheme for satisfiability modulo theories","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q438578$7F2FA57C-BFB8-4022-869B-E4FCC4B855DF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9d1a36c82a692297767e03b5bd6c368e7db62ed1","datavalue":{"value":"1430.68401","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438578$37F0217F-29A6-408B-861B-47C2584949F0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"da9d0bb1bba7f8d78f26f8b0456c3cbe905220ef","datavalue":{"value":{"entity-type":"item","numeric-id":438577,"id":"Q438577"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$D4F5C4C6-E3C6-4112-9883-32364FA862C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"dbb66b347a8501d3e88bb4fc6db185a6021261a5","datavalue":{"value":{"entity-type":"item","numeric-id":167063,"id":"Q167063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$6A2F785E-3A63-4E4F-BDDB-CFAA47A1BBB3","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":"Q438578$5DE55687-BB52-428E-952B-4537840F7E5C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6c7ad691786690cf86127845d28cf47311748286","datavalue":{"value":{"time":"+2012-07-31T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q438578$9AEB108D-E201-4949-8144-6C1121CC72F8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438578$F4AD90D3-A19F-442B-936A-8F8A37CF83D2","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3de6ba161f6bf52d7f0aaad81cc51b95da5c15a0","datavalue":{"value":"6062064","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438578$9D4C8AC7-CD5D-48EE-9324-1C69E7038439","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1254a7c01d2970b87da2854c1fde40c268a1f55d","datavalue":{"value":"satisfiability modulo theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q438578$851AD0F0-5988-4689-8E36-4C0D573ED331","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"67ffa9831e001db05d16b4e8c771f35f579f25e3","datavalue":{"value":"instantiation-based theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q438578$A08BC4EB-F6B7-4AE7-A98D-FF94D005E3DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dfd2ae52b3325778b0c72742b08c947a3c4a2c65","datavalue":{"value":"decision procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q438578$866E4449-1134-45B8-9868-E0EA0B7A127C","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a2e4454b50103c6e6499c664726a4f18fc7c5af5","datavalue":{"value":{"entity-type":"item","numeric-id":16784,"id":"Q16784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$1AEED589-043D-4F76-86A5-BDFE5D841553","rank":"normal"},{"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":"Q438578$DF39C67D-F9AE-4DCF-A322-D603B7F9BD47","rank":"normal"},{"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":"Q438578$B881D91E-BFF2-4AFC-90C2-C80D7204EB8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2822825cdea331aa7c0ec2c340c1eb36d62db00b","datavalue":{"value":{"entity-type":"item","numeric-id":17123,"id":"Q17123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$3DF524E0-000B-4055-975E-1920B872A920","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":"Q438578$8B0BF93C-CC27-41C7-B234-00569BC7EFA5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e3077241cf9dd3ea3dc1ed3e3664e85ede45567f","datavalue":{"value":"https://doi.org/10.1007/s10817-010-9200-3","type":"string"},"datatype":"url"},"type":"statement","id":"Q438578$7688A99C-B629-4056-A6B1-E05ACA3D0167","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"98cb670c97efeeb3296d5e234efaa0e188291b99","datavalue":{"value":"W2041790367","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438578$CE474C1D-42E9-4A1E-AF04-5D84D2CBCAE6","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"280010c88ea3654588239b55152e0eb25171e531","datavalue":{"value":{"entity-type":"item","numeric-id":1041587,"id":"Q1041587"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$5F60818E-B5FE-4056-B83C-25C181FA289E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"103360585a9bffb1c1cc70bf60b5d74438ed3255","datavalue":{"value":{"entity-type":"item","numeric-id":1401930,"id":"Q1401930"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$79338ABF-2841-43CB-8C8E-19B1650BF283","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0a351897245977aa0d098a2219b09f6d20cfa230","datavalue":{"value":{"entity-type":"item","numeric-id":2751360,"id":"Q2751360"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$D6984D5F-19C9-43B5-B1C2-07D930121FDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4aefe5e0f2b827afb25f0a8067d25c4a893f91ca","datavalue":{"value":{"entity-type":"item","numeric-id":4304492,"id":"Q4304492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$44F07A49-E6FA-4BA7-8B67-391F34F6E685","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6dc64d6d31493ac74da4f6c177f509ec4a9d4b14","datavalue":{"value":{"entity-type":"item","numeric-id":4804899,"id":"Q4804899"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$A72F785C-D36F-42DC-BFD1-C47E6F85C7EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6386f9d9d555cce966644dfe59274fe1062f77ec","datavalue":{"value":{"entity-type":"item","numeric-id":5450569,"id":"Q5450569"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$B1B61838-3AEE-41B1-AF21-3D21D34F1967","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"52b18a75aad9c9a7a5a4368c62a0e4bea68bf145","datavalue":{"value":{"entity-type":"item","numeric-id":1041591,"id":"Q1041591"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$35CC99DB-0645-4744-98AC-070A8F67A1A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cfc74a420b6b7ea54906573084cfacb776d08039","datavalue":{"value":{"entity-type":"item","numeric-id":3613431,"id":"Q3613431"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$C6AE2838-E33F-4853-A6FA-32F8E8D0C5C9","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":"Q438578$D5FA3864-3473-4503-85C5-D3AA5963C7A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f2b1ebc1ae7ffc3042b5e838a24da8662374478","datavalue":{"value":{"entity-type":"item","numeric-id":5898633,"id":"Q5898633"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$109597AE-B66A-48B9-BAE4-53ED18AF54B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bdccc5d83f7311582ae4e1c48da92b5c9b5c7298","datavalue":{"value":{"entity-type":"item","numeric-id":2559426,"id":"Q2559426"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$DD1872C2-430F-4601-B3FC-D5386AA73A7E","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":"Q438578$7DD2262B-DF6B-4906-A1C3-39B42CDD1B28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c0e6b90c16ae5fa1eac19212a306cb84ffec72b","datavalue":{"value":{"entity-type":"item","numeric-id":5613969,"id":"Q5613969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$9BA25914-53BC-4560-AC2A-BF5F9888AF31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5a8f27245772c2159d3ccf93c502a4163695153f","datavalue":{"value":{"entity-type":"item","numeric-id":3541724,"id":"Q3541724"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$F668FC8F-12D8-4AC2-8E10-A96BC4CFA1A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b4f714dbb33bba32b50777c1d77c1cb7ff5fe56","datavalue":{"value":{"entity-type":"item","numeric-id":3608773,"id":"Q3608773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$95DAF60B-CC3E-483B-80CF-17C21D0B77CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1daf6c1b27d4e2241acccb436e068cfc4f24ffff","datavalue":{"value":{"entity-type":"item","numeric-id":3546294,"id":"Q3546294"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$9D6AB7F6-495B-4E3E-8F6A-C05C44A3F98F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ccc4e7f4906537705fb3b0b96d8e415aef39b2cc","datavalue":{"value":{"entity-type":"item","numeric-id":3582696,"id":"Q3582696"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$5692389E-5B7D-4C3C-8E97-6C24E0082233","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae611ccf26d614d6f5569c32d95f83372cdd7983","datavalue":{"value":{"entity-type":"item","numeric-id":5311286,"id":"Q5311286"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$8E225E78-8C09-4FE9-A0FB-973BA6AB9B8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"90d27466745eba57837a04b18173a99a47f5ad2f","datavalue":{"value":{"entity-type":"item","numeric-id":1037401,"id":"Q1037401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$7B707CD3-8A0D-4525-B964-80F762374357","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f426d61b5e73f09c762af22502a76e1d6d446b2d","datavalue":{"value":{"entity-type":"item","numeric-id":3636870,"id":"Q3636870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$7EEDE284-490D-4640-867B-4AEB6D573ED0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"935217a246ae5adafd48508e6fe779ec4121b228","datavalue":{"value":{"entity-type":"item","numeric-id":5387918,"id":"Q5387918"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$DC74D6BE-AD46-48E2-AEDA-9FB8043799E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"88fba5a1fdfac74b8e0dcefe0e56f5b10792486d","datavalue":{"value":{"entity-type":"item","numeric-id":688547,"id":"Q688547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$CF3BB7EF-BC75-4BA6-B2BE-7A8D4A848187","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0107293e5a161b96a51a1cd082064c48cc78da52","datavalue":{"value":{"entity-type":"item","numeric-id":3608782,"id":"Q3608782"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$E6EDD579-CFD7-43B5-B238-77A177F2F670","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f00589542fdb6ec4fc401e47318165d5bad4f817","datavalue":{"value":{"entity-type":"item","numeric-id":1581853,"id":"Q1581853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$C1E5FE90-AA18-4EE4-802B-10E088721EB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"601ec2c706ddf45de31ee679a12674e1ca489252","datavalue":{"value":{"entity-type":"item","numeric-id":4916225,"id":"Q4916225"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q438578$59AF130D-87F0-4BD2-B8D9-62F1B2A032CE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"137c462cde3818c086fc1fb293b7523ca0f49f43","datavalue":{"value":"10.1007/S10817-010-9200-3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q438578$5250DEDC-0316-4DAD-B91C-C30979E7CE06","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d5cde24298f23a5b7bc7c7603ce121b3af6925fa","datavalue":{"value":{"entity-type":"item","numeric-id":1944184,"id":"Q1944184"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d95ba85290d829d77d5fdd1867ea1d8ea454cec7","datavalue":{"value":{"amount":"+0.8560587763786316","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":"Q438578$71229D01-7CCC-4044-A58E-2E00CCE218BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3af69d6db622a43b899210ae0c79af2cf40708bc","datavalue":{"value":{"entity-type":"item","numeric-id":3582696,"id":"Q3582696"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4a15adc56eeb9d9df278810d05a10dd589a301f9","datavalue":{"value":{"amount":"+0.8367156982421875","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":"Q438578$91ACFF41-F956-441F-8785-F0E49814826C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"709211d935c435620f867d257bf161ec3a85cbd6","datavalue":{"value":{"entity-type":"item","numeric-id":3636870,"id":"Q3636870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0dcf02599a90ae6bb55d94ab0dd2f479fd86b397","datavalue":{"value":{"amount":"+0.7914018630981445","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":"Q438578$1C49EB09-5D8F-4C90-99A0-7A3A8944D5C7","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":"c59237381eab40555dcb3888dc1d56a0555c0a57","datavalue":{"value":{"amount":"+0.7763352990150452","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":"Q438578$734AA478-15D3-45C8-9D1C-F3D70C6E4923","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a163d4150362be8e1e2f5d5bb6dfb8185f2a5266","datavalue":{"value":{"entity-type":"item","numeric-id":5387915,"id":"Q5387915"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5b8b08213d74e80cb5d88612098c8b8dcbfb2022","datavalue":{"value":{"amount":"+0.7740508317947388","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":"Q438578$733B5D76-5CE0-431E-9B21-BBC91171A162","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"An instantiation scheme for satisfiability modulo theories","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/An_instantiation_scheme_for_satisfiability_modulo_theories"}}}}}