{"entities":{"Q2843009":{"pageid":2853729,"ns":120,"title":"Item:Q2843009","lastrevid":83849621,"modified":"2026-05-07T12:59:32Z","type":"item","id":"Q2843009","labels":{"en":{"language":"en","value":"Automated reasoning service for HOL Light"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6197178"}},"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":"Q2843009$2C2034A2-17C5-414B-88EE-E4D2F5D1F505","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0c85d2778e42eeb0f34da7f91398d439846996e7","datavalue":{"value":{"text":"Automated Reasoning Service for HOL Light","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2843009$17370D9E-B9A2-4806-9DCB-C90B4E709267","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"cabd59f57c8f406291745d14ba7ecfce4e29fcbe","datavalue":{"value":"1390.68576","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2843009$B11DF22C-92C4-4AB3-B8B1-440418CB5D9A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0d51ea5e9395e43558b5f2f522060bff93030dc5","datavalue":{"value":"10.1007/978-3-642-39320-4_8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2843009$0324803F-D9D8-424B-A3A1-F0114E3E5F53","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6ad6a046b48bbe4ab777309f1d5c19b5fc7dfbda","datavalue":{"value":{"entity-type":"item","numeric-id":286799,"id":"Q286799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2843009$3073E38D-D1AB-4CA8-8626-0F0E762F2E46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"dc204e2e78d924e815f2b640ec35c8c2356ad41f","datavalue":{"value":{"entity-type":"item","numeric-id":286786,"id":"Q286786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2843009$CEDFBF87-A037-48C4-BA59-21AA61CFAFD8","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":"Q2843009$6C061091-DBEB-4E91-A80A-B245EEAA67CF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"381d46b885a4d4a1524f419ca9a0dc18cd8f863b","datavalue":{"value":{"time":"+2013-08-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2843009$030422F9-ABD4-4DC9-B740-0426E43BCF1B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2843009$B4425136-BE5D-4830-9EF2-4BAA6BEA7169","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"33942bcde6235be95540ba0d0c14df2b390f273e","datavalue":{"value":"6197178","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2843009$498CACC1-C6BC-4A6C-993E-177F004FBC3A","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"43f7c4ee5068daf82f8bffbb0f7510a5f16faf63","datavalue":{"value":{"entity-type":"item","numeric-id":16615,"id":"Q16615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2843009$D1FAFCA1-A52F-4ACC-8382-DF92E454B266","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7cccd35b34888307d4ad7b137783609eb5c56b79","datavalue":{"value":{"entity-type":"item","numeric-id":16825,"id":"Q16825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2843009$BA05ABED-C200-4DA5-8948-539F0AC262BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19c3232540dc15c9350e8393498317de25361cb2","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2843009$5908721C-CE8F-49A6-B7EE-D1061A3E4519","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8376bcc90e7c7f009563b97a4560743162f2cada","datavalue":{"value":{"entity-type":"item","numeric-id":22158,"id":"Q22158"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2843009$8AE22C8B-0B82-40D4-AD0C-5484B86DA859","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":"Q2843009$6F48C0D1-0196-462F-AFB6-5A83BD495B2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c7cbb37e14a01458626c5623c37a9141435c8062","datavalue":{"value":{"entity-type":"item","numeric-id":19250,"id":"Q19250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2843009$F30B9B87-4B1C-4FB6-BE87-BCC3BFC0845E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bf8fe40ec0751f683b8f31fdc6f7f38f8aa07409","datavalue":{"value":{"entity-type":"item","numeric-id":13328,"id":"Q13328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2843009$5EAD36A1-5EE9-40E8-882A-69A7AF651528","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1017108dce3983431546a14c274f65bc4aaae70b","datavalue":{"value":{"entity-type":"item","numeric-id":22154,"id":"Q22154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2843009$DF489D6D-9248-4607-931A-CD644AE27F51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"62af2c5e450adf37bd9acb47c5a55b60b68447ea","datavalue":{"value":{"entity-type":"item","numeric-id":22241,"id":"Q22241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2843009$ECBF3975-C950-4E70-9611-984E6CADC8A3","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":"Q2843009$0BB104AF-83DD-46E4-9D73-776E7F128106","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2843009$25F62DB1-4D06-4DEC-91FE-FB336EF20DC6","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":"Q2843009$BD74841A-142D-43AD-A312-325CB61FB9EB","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e05024af51ebcdd1ac1580069bdd59c8b2d7ca69","datavalue":{"value":"https://doi.org/10.1007/978-3-642-39320-4_8","type":"string"},"datatype":"url"},"type":"statement","id":"Q2843009$C38C9020-71B6-4573-8DA1-6B4AEE67DD0D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a61e68b952a7b2231faa799684755d4e402dd336","datavalue":{"value":"W2102819792","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2843009$AC0BC5C2-2B32-4CDD-86EC-CE8D5DBC4C02","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"3420d953df4247cdcc5cec35a233e3a2841058c3","datavalue":{"value":"Q108482172","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2843009$43FFAA96-9B66-4516-AECA-9FC4C0F49484","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b296e1372a277c764684803a4b4b78039b98cef4","datavalue":{"value":{"entity-type":"item","numeric-id":2018657,"id":"Q2018657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5ef2327c6d2b11814dc600be962c16721a88e898","datavalue":{"value":{"amount":"+0.9461746215820312","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":"Q2843009$032C5B75-7D52-46F8-A9DE-76CBA7B2C263","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"62eb5673352ddfd5c999328fdcfb0b637fbd9630","datavalue":{"value":{"entity-type":"item","numeric-id":2351415,"id":"Q2351415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"400c8454788555d8bcaf62ddbf793a7af9d15461","datavalue":{"value":{"amount":"+0.810215950012207","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":"Q2843009$F339B6F5-1E1D-4117-9B73-D24B8E9C2AD5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b1dfeb4f58629a3de8f2170811c634bc1408f23d","datavalue":{"value":{"entity-type":"item","numeric-id":1945905,"id":"Q1945905"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dbc19ae658ed1325809d042eb8233a5107df6672","datavalue":{"value":{"amount":"+0.7826626896858215","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":"Q2843009$253DD9EC-E980-4DE9-98DC-83C5BA3B1A17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d076348236722044a3aec87ce8b8b223d0d096f1","datavalue":{"value":{"entity-type":"item","numeric-id":3460068,"id":"Q3460068"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8c5a03d360f567ed028a86166c886266923b48a0","datavalue":{"value":{"amount":"+0.7532488703727722","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":"Q2843009$73EBA3F1-4DC5-4FAC-9A32-70C4F6429935","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f5240345605b6df958dc529fb8dc1a54b30d31b3","datavalue":{"value":{"entity-type":"item","numeric-id":3183517,"id":"Q3183517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"445beb156528e47f76685cbded2938eee8d70445","datavalue":{"value":{"amount":"+0.7528691291809082","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":"Q2843009$858967DA-5459-4C1E-AF6F-B5CF3A167A58","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Automated reasoning service for HOL Light","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Automated_reasoning_service_for_HOL_Light"}}}}}