{"entities":{"Q3578390":{"pageid":5608294,"ns":120,"title":"Item:Q3578390","lastrevid":88430675,"modified":"2026-06-04T14:30:15Z","type":"item","id":"Q3578390","labels":{"en":{"language":"en","value":"Theory-specific automated reasoning"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5758213"}},"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":"Q3578390$EC719AC3-A22D-493B-A3C6-ECED9C3CB9A2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7e044d44fca38adac3daba34219441eb6a184f19","datavalue":{"value":{"text":"Theory-Specific Automated Reasoning","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3578390$134C8937-7864-420A-A898-EBB30A6C2616","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5d0875ee2e226fd12ed403318dc7fac8a2fb0ad6","datavalue":{"value":"1285.68146","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3578390$2142DA5C-E59B-45DE-BE21-7F5C3A725742","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"fd880befd9511b2e73ef4536c69141938452a5e0","datavalue":{"value":"10.1007/978-3-642-14309-0_3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3578390$9BE1901A-E79C-4F59-B8C9-CF657C4CAB4A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fb6915ece1ff0e3c04b1478b9a756ad0cf2910cc","datavalue":{"value":{"entity-type":"item","numeric-id":167067,"id":"Q167067"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3578390$1F759438-AF1E-41A3-8942-61700DDA15AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9faadbd22dd8b1da3be6dbb593d6df9253bd99cd","datavalue":{"value":{"entity-type":"item","numeric-id":1248615,"id":"Q1248615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3578390$2FA7980C-FE9B-44C1-BEF8-2AA8988C4A24","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3578390$909BBD48-D273-435D-A0FE-DFD1C0B8092C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"49725197d5403193e6793b874c212de8a1d5fa7b","datavalue":{"value":{"time":"+2010-07-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3578390$CB580201-DD53-405C-B85B-D7E6BDA824C2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3578390$C7232049-A25C-4606-8B86-20D62F79DC21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3578390$CB8EEE7E-E7F7-48BF-A65B-D39C7F860E8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7d6d1b45c606677a96fadd625efc72a171c20037","datavalue":{"value":"03E99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3578390$D384AD00-804D-43D2-8755-BEDBC31CA4F4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2e8707af664a76bed97846271a64f01faacdf639","datavalue":{"value":"5758213","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3578390$684294A5-94B5-46D0-8277-A3069D28606F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6a78675f0dcb3af511ac1d4dfa61901e828bcb8","datavalue":{"value":"proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q3578390$84610241-CC63-4A47-BBC6-B1F64E0916A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f3018f13ec4565557bf025633f394ef25a05fe3b","datavalue":{"value":"decision algorithm","type":"string"},"datatype":"string"},"type":"statement","id":"Q3578390$5E0A57B4-3EE5-426C-A4BD-9D1F089D296D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddaa2c962e34c4a9ceec327eb778c44347865b10","datavalue":{"value":"inference mechanism","type":"string"},"datatype":"string"},"type":"statement","id":"Q3578390$D597C1AF-08A7-43C1-9E42-A35B92449EFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b36a4092864d39bf9c99c5936b3d1261e44b9950","datavalue":{"value":"set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q3578390$111AC9A0-5FF1-479C-B9E6-C1AD8E701228","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":"Q3578390$23002119-1421-48EC-8516-8B2B42A72C27","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ee1ade58731a6622054e7651417032c309670eb1","datavalue":{"value":"https://doi.org/10.1007/978-3-642-14309-0_3","type":"string"},"datatype":"url"},"type":"statement","id":"Q3578390$C1CC99E7-B3B1-413F-AB49-61D5045A0157","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"6f1ed77afebd8e97511d9d5269a42dfd3a8c9084","datavalue":{"value":"W1809302967","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3578390$EDFBA23F-3E60-4075-9582-1FBEBCB527AD","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7d53e3269671c3b829332645636422f0534f2837","datavalue":{"value":{"entity-type":"item","numeric-id":4707766,"id":"Q4707766"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"59b0fbff5666dea6af11d9beae25a210b12efecf","datavalue":{"value":{"amount":"+0.7803291082382202","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":"Q3578390$3BEBF5CD-8F62-4371-9050-4EA8973B6927","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"039c873276c470bee9e8337c738ab0cb44cc25ee","datavalue":{"value":{"entity-type":"item","numeric-id":3812202,"id":"Q3812202"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b407a312a774a4dff3827ea862d5bddc1a9e61fb","datavalue":{"value":{"amount":"+0.7413133978843689","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":"Q3578390$6E6C5CEE-1E03-43C1-8310-5C7AA93F9FC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3d8213c84e722b981af05319a6ca2089cbbe9522","datavalue":{"value":{"entity-type":"item","numeric-id":2457343,"id":"Q2457343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3fb7290c29f5eb8bb2e95b90f210423e3bcb00f8","datavalue":{"value":{"amount":"+0.7366999387741089","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":"Q3578390$EC8EBA38-9E92-40F5-BB1C-0D74B6D85582","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1ba1fab2dcbd62ed944c931318abb685d95c7a56","datavalue":{"value":{"entity-type":"item","numeric-id":5927987,"id":"Q5927987"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"de348f7667fa96eba02b03095dd567ce6663d351","datavalue":{"value":{"amount":"+0.7358430027961731","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":"Q3578390$05681079-ADF3-462F-BFA6-8F8CD4715D3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"86850ded6f45d5b101dc64f62f56e07fc50ca10b","datavalue":{"value":{"entity-type":"item","numeric-id":1914165,"id":"Q1914165"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3e94370c38d7e9387187b667bc5514046cc1dfb7","datavalue":{"value":{"amount":"+0.7328299283981323","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":"Q3578390$A4DDD7BC-2CA8-48F1-A57C-94CE158E5C6F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Theory-specific automated reasoning","badges":[]}}}}}