{"entities":{"Q2870120":{"pageid":2880840,"ns":120,"title":"Item:Q2870120","lastrevid":83598335,"modified":"2026-05-07T09:16:26Z","type":"item","id":"Q2870120","labels":{"en":{"language":"en","value":"HOL Based First-Order Modal Logic Provers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6247431"}},"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":"Q2870120$F801FCF3-1FF8-4890-90F9-93B9AD8E8505","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f1bb0d05d38378d7eefa373d4c834526d62d9679","datavalue":{"value":{"text":"HOL Based First-Order Modal Logic Provers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2870120$49C4EA88-BC78-4671-85A2-65ECD0C470A6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d71ce04031e14425703a6f8fa940c270f9df121c","datavalue":{"value":"1406.68103","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2870120$F4910C12-29CB-48F2-93AC-638860BB1B4A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"79379e0e733027316e9a918e6f0a24b50f2b7bd2","datavalue":{"value":"10.1007/978-3-642-45221-5_9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2870120$5723CE7F-D495-432A-9FD2-827DB016EA9C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a525f7cd8b191ac2b9090383b0dabde3689f4ff2","datavalue":{"value":{"entity-type":"item","numeric-id":287280,"id":"Q287280"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870120$A3D9B9D7-17B2-4A97-844F-AAB302147B99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"67bd31a228240db87ccebadcd822c2f02977875e","datavalue":{"value":{"entity-type":"item","numeric-id":877895,"id":"Q877895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870120$B9553446-6499-4492-8167-9EA103C99744","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"23864e2be568bb8a6a4b0526f5a5216348320070","datavalue":{"value":{"entity-type":"item","numeric-id":2870110,"id":"Q2870110"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870120$9258F3A9-1589-40BE-B8D3-6F4B04F9195B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7cbcb8793fff212e9a1970116a64b7b67cfe92e5","datavalue":{"value":{"time":"+2014-01-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2870120$97CCEF0A-6C84-4103-A813-3778F17CEDB4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2870120$51B8523B-CA80-4924-B594-2193D8A82473","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2870120$FF90B76A-2209-4A49-AA54-73786260AF9A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"271716c70f53da93bba1e5bbecbd113d49c9f1e6","datavalue":{"value":"6247431","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2870120$9345B2C9-4731-4A17-A498-527F9D0CB05C","rank":"normal"}],"P1463":[{"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":"Q2870120$F7D39CB1-BE63-426E-A39E-D6421A32D0CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8617a61c90a632f23d3851deb94e1069d2479a78","datavalue":{"value":{"entity-type":"item","numeric-id":13268,"id":"Q13268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870120$A998CE7A-7EA8-41A2-AD3A-C9C6A00268A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ae510ff9d7026cdfae7484e5c88af62cffb92c77","datavalue":{"value":{"entity-type":"item","numeric-id":21735,"id":"Q21735"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870120$D9CC4C5C-8AC0-4989-80D3-82C6E718370B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"824e66560bf30b02805a91f52441dbc38109d38d","datavalue":{"value":{"entity-type":"item","numeric-id":21736,"id":"Q21736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870120$7051D90D-1328-4B74-B9A0-50E3B4F9A367","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d83b780839e730b0091759b62a50b0f768844ed7","datavalue":{"value":{"entity-type":"item","numeric-id":21894,"id":"Q21894"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870120$A0F7D7A9-030B-477B-9E2F-A7C729B3E46A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"53f05770302a5e6870dfe9aed5a78e67d74a3e9b","datavalue":{"value":{"entity-type":"item","numeric-id":25217,"id":"Q25217"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870120$BAD1F687-DCFC-4A7E-92D2-6C58E7E22538","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ecb36fec89ff827cd73a8ca1a85f36a2e419c34e","datavalue":{"value":{"entity-type":"item","numeric-id":13377,"id":"Q13377"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870120$38677A45-9A06-43F0-9C30-883601756DD9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870120$967D8B60-EF10-4A6B-8607-5EEB58A7D5BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"491e4169c914222bc349264f15b36cbf2c3ef446","datavalue":{"value":{"entity-type":"item","numeric-id":18920,"id":"Q18920"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870120$A9BC81F8-F8A5-462E-A05F-40AE71C8609F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bec249a9f2158ac9024acac21e3dec3b5d305ee5","datavalue":{"value":{"entity-type":"item","numeric-id":29522,"id":"Q29522"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2870120$377AB8BA-8842-400D-9E7C-9724D6DECAAE","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":"Q2870120$D6671999-C602-4A8D-806C-F9B1EDF9DF2D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"706c739fc10421dfeee28a322763191af29d93cd","datavalue":{"value":"https://doi.org/10.1007/978-3-642-45221-5_9","type":"string"},"datatype":"url"},"type":"statement","id":"Q2870120$FB46AAEB-4978-4AD4-944E-7E5A71D2FC36","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5cfaafa86e3b128ed08203f1792416b9e8aa3c8b","datavalue":{"value":"W2268873381","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2870120$60D33940-F8D6-4D9D-A495-49D6825C9795","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"006b7fde6af592f6799db7f14c1f8600cd6b606c","datavalue":{"value":{"entity-type":"item","numeric-id":3457212,"id":"Q3457212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e834e08f281860d27b44228b40fe6a1df642971c","datavalue":{"value":{"amount":"+0.926713","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":"Q2870120$FCB2B9B8-72B8-4599-AADE-AEF8ABE8992B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"44900fea966451a6666b697ebfa2032f7c577d5f","datavalue":{"value":{"entity-type":"item","numeric-id":5413353,"id":"Q5413353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1eb437e95b1cdf44b646a3f4a02ae50a988b66dd","datavalue":{"value":{"amount":"+0.92434704","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":"Q2870120$DF9E39DE-4EAA-41F7-93AC-7798AB5E7E35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8d6d293412ec27137e9c499546b1328aad012c7d","datavalue":{"value":{"entity-type":"item","numeric-id":3133155,"id":"Q3133155"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e17a857538a87e34743160f03248ce1ee02ea7bf","datavalue":{"value":{"amount":"+0.9061805","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":"Q2870120$65E29185-51B9-47F9-B706-9C9BB182AE01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f619466380248c55ace1b70c6c55c0d678caba54","datavalue":{"value":{"entity-type":"item","numeric-id":4247082,"id":"Q4247082"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"287f1c714dcf53eda11906ef07084024b901f9af","datavalue":{"value":{"amount":"+0.9028764","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":"Q2870120$C3B9E458-361A-48B4-801B-48BBF9ED0C68","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"52b0949bca6460ae1f5912e2961866309910fefa","datavalue":{"value":{"entity-type":"item","numeric-id":6162119,"id":"Q6162119"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b300481f4d4d7d2af14010556228f1b1e0055286","datavalue":{"value":{"amount":"+0.90152055","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":"Q2870120$D81D807A-85E6-41D5-8FB6-7B87FF137238","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1ed030b74f186a9c7e144c1a5c1bdbc2e1e44f57","datavalue":{"value":{"entity-type":"item","numeric-id":622627,"id":"Q622627"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"10478cfadd0019e60c3f9ad038c79e04d77ef1dd","datavalue":{"value":{"amount":"+0.90150833","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":"Q2870120$A44090DB-0048-4214-8492-00853729D6EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d086b4b51064d8e06f38be082ed9cc17ef292a07","datavalue":{"value":{"entity-type":"item","numeric-id":6535436,"id":"Q6535436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"541ac8bd47383132f5205253e27153e983da701a","datavalue":{"value":{"amount":"+0.899618","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":"Q2870120$2DEBEF9D-10F4-4088-B9D9-113241EAE2A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5ddc51bc6e27a4569a17968485e70f6d1bb0171b","datavalue":{"value":{"entity-type":"item","numeric-id":1870904,"id":"Q1870904"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"541ac8bd47383132f5205253e27153e983da701a","datavalue":{"value":{"amount":"+0.899618","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":"Q2870120$E73FD33D-BFEF-46EC-809B-9CDFF7D3EA31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"90d50e1c0df666fa91adb1a99dc10e55d393c6d9","datavalue":{"value":{"entity-type":"item","numeric-id":4916086,"id":"Q4916086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a86840bb8bce8091ee255011f001f1d05b199aa0","datavalue":{"value":{"amount":"+0.89935946","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":"Q2870120$40F7C6D6-412D-4151-ADD3-C365BF73A998","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"HOL Based First-Order Modal Logic Provers","badges":[]}}}}}