{"entities":{"Q879370":{"pageid":881218,"ns":120,"title":"Item:Q879370","lastrevid":65075592,"modified":"2026-04-12T00:09:34Z","type":"item","id":"Q879370","labels":{"en":{"language":"en","value":"A few exercises in theorem processing"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5151784"}},"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":"Q879370$52F7F177-64A4-4AEF-9BA3-4513A2249937","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f1d07255e7a60378f0bde98a91f3220a059f5f1a","datavalue":{"value":{"text":"A few exercises in theorem processing","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q879370$D66C54CF-5570-44FF-B624-55A6F624103C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"487918ab127a3b296ab279592b5a45fd4432677b","datavalue":{"value":"1111.68114","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q879370$9A473F66-DDB9-4EE2-A044-A9F9D09C1F38","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"baf86fd7bb8ef71035036158a7ec4885e7ee77fe","datavalue":{"value":{"entity-type":"item","numeric-id":794941,"id":"Q794941"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q879370$DC4F149D-986D-4F65-A2DA-63D7FE8401FC","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q879370$F251DDE2-3D5A-4746-9ACE-7A37389BACEA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"cbd0eb8b100807c851c8df9ae7f8fa5376f95dfe","datavalue":{"value":{"time":"+2007-05-11T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q879370$CF50BCFA-B035-4407-B80C-146DB698D524","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q879370$2E4F314F-CF79-451E-8D8B-D12B220F57DA","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f5b75b772fed3f41ae02422966a07926c5223c3d","datavalue":{"value":"5151784","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q879370$83B2506E-700F-423D-84FA-CD2DE46FB046","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"365e72d6093f16a8523f1adbfcc192c726048515","datavalue":{"value":"theorem processing","type":"string"},"datatype":"string"},"type":"statement","id":"Q879370$EDADD9CD-0202-413C-945D-D9BD0C60E561","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"edb9c7b6e5b36868a8fe6f158d3dcde5900d8c06","datavalue":{"value":"derived inference rules","type":"string"},"datatype":"string"},"type":"statement","id":"Q879370$4A3F15C3-D09B-4649-8413-902BB365E650","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"176130281ad96d9ae242c0ccc4fa11b97757fa0b","datavalue":{"value":"conversions","type":"string"},"datatype":"string"},"type":"statement","id":"Q879370$CA3ECD96-0AF7-4E37-BDE6-63488CF73365","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"323010e94a2c00a4cdc3c5a5684770a8be2fdc6b","datavalue":{"value":"list processing","type":"string"},"datatype":"string"},"type":"statement","id":"Q879370$5FD8EC18-B0DF-4D86-9143-30521B56DBFA","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q879370$94D72283-168A-46AF-B86B-12B995E57152","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q879370$1F0FBA31-61D8-4A52-9F35-875CD7E855D8","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":"Q879370$8E39D7E8-67D6-4E9F-8528-290C1A81C026","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a0497a28a1a1cdda8a3de3230d687e090653b85d","datavalue":{"value":"https://doi.org/10.1016/j.tcs.2006.12.037","type":"string"},"datatype":"url"},"type":"statement","id":"Q879370$6F0CB3C6-170B-4CF1-B281-C90BBA51E0EC","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"772e3f0ac5a925511b9c85618c9dca566fb3f02c","datavalue":{"value":"W2067501613","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q879370$8242F742-CD59-44C5-9981-0C56517B7773","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"df6d745c28f41f3f6887e89cc1ca892988e70309","datavalue":{"value":{"entity-type":"item","numeric-id":5287513,"id":"Q5287513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q879370$97B8E472-94CB-4EA7-A11C-5AFA0EDFE728","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cc8abb92210655a5bd4143cbbadd6eadb52d635","datavalue":{"value":{"entity-type":"item","numeric-id":1801222,"id":"Q1801222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q879370$B9884F1F-2DC7-479D-A891-868D15CC2D28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6496304f13783e82d12a275120aa4626825ea47b","datavalue":{"value":{"entity-type":"item","numeric-id":4231030,"id":"Q4231030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q879370$A0648D42-CD4C-43B1-AB03-292233D11150","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"35852691e725c71cf8e921b7748b4e2b09da6624","datavalue":{"value":{"entity-type":"item","numeric-id":800739,"id":"Q800739"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q879370$3425C167-E59E-4DE5-9DDA-A9BCD832F1CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"085f2f402bb0aaa918a693e06aa64da16c2193f2","datavalue":{"value":{"entity-type":"item","numeric-id":5687569,"id":"Q5687569"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q879370$27762640-A76F-47A7-BC0B-0CD811C0CFA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"464b1870bccf13dbc5906b6fdcbedf4f91a8bf40","datavalue":{"value":{"entity-type":"item","numeric-id":5588137,"id":"Q5588137"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q879370$AA407717-5932-420F-8A3D-E62FD76F5827","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"906f04569ac91373dc4639a67220d421acb054aa","datavalue":{"value":"10.1016/J.TCS.2006.12.037","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q879370$F312214C-3003-444E-8CAE-1C2B8BBA6233","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b31b77fca7c9b8ba84a5adfb7106757a93e764bb","datavalue":{"value":{"entity-type":"item","numeric-id":3696549,"id":"Q3696549"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6a1a3f8744017398f01e61c997e13119f624dd29","datavalue":{"value":{"amount":"+0.7704699635505676","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":"Q879370$DC82B6DC-5E90-4228-8C46-F7AE983A03AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fe0ff340996ef479adc8088e2952e35568f687e4","datavalue":{"value":{"entity-type":"item","numeric-id":2754029,"id":"Q2754029"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ea5dc4848f9f23b43f27ef7a758c0b5319de6285","datavalue":{"value":{"amount":"+0.764559268951416","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":"Q879370$A088D8CB-6D39-4A7B-8508-0BC383AF8A90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"80da2311e24f203113d173f62f7fb303bd7ca4e3","datavalue":{"value":{"entity-type":"item","numeric-id":3024889,"id":"Q3024889"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1291844e5b929b318b76a70fa0f7d0065db2317c","datavalue":{"value":{"amount":"+0.7424946427345276","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":"Q879370$B251CA52-72D1-4777-B965-430B8ECC9905","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4975addb4905a856dc84fcaa166c071e9d04c5e7","datavalue":{"value":{"entity-type":"item","numeric-id":800739,"id":"Q800739"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"abddc7908e4012f9a85012d49680393a19016749","datavalue":{"value":{"amount":"+0.7418118715286255","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":"Q879370$A31045C8-F3A1-479A-BA1C-91212D0C5435","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1b18f1bcee5a559e76e86ee84dd5601244af54f6","datavalue":{"value":{"entity-type":"item","numeric-id":909488,"id":"Q909488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"382dad9abe2f3963f9c763de4f6b95984659e83e","datavalue":{"value":{"amount":"+0.7390159368515015","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":"Q879370$80ABE88F-1D51-4C74-BCD4-3A82E483C21C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A few exercises in theorem processing","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_few_exercises_in_theorem_processing"}}}}}