{"entities":{"Q1987736":{"pageid":1998478,"ns":120,"title":"Item:Q1987736","lastrevid":53710349,"modified":"2026-01-25T14:30:51Z","type":"item","id":"Q1987736","labels":{"en":{"language":"en","value":"A verified proof checker for higher-order logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7189663"}},"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":"Q1987736$BF163E77-DBC1-49EC-B3D5-BF0F364C77E0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"17b5cccaab0737d7a90aefc7af84b1301dddadce","datavalue":{"value":{"text":"A verified proof checker for higher-order logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1987736$A1D3E299-8D7A-487E-ADDD-CA688BD60DCA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8262962fcd675a0ea7b4cc5923ff4d6cea7d9126","datavalue":{"value":"1433.68527","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1987736$6E56A775-3BB1-4CAB-92A9-67F2ECAAAFC6","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"48bf256cb2060adcce83d6ff0339ba7814ac6cab","datavalue":{"value":{"entity-type":"item","numeric-id":1799127,"id":"Q1799127"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1987736$CE9E9BFE-8F95-402D-B0CE-B97D05907259","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"2532b82fbfd494721e144e8b872f80867d7316e9","datavalue":{"value":{"entity-type":"item","numeric-id":246441,"id":"Q246441"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1987736$8C2AA9C7-A4F6-4864-B7CB-F31B0082D06B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ebf3996599473c7cbdf44de21918855753346b67","datavalue":{"value":{"time":"+2020-04-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1987736$A065A06A-8339-4530-8115-436DACF781AB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1987736$B48C1AEB-1E10-44BE-8B43-BA16FF53493F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3f6d4b3012578fba2d8ab6b9e39d328cad9def57","datavalue":{"value":"03B16","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1987736$0D7A3972-6BAD-4F04-8FA3-9AF09FD4BCEE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ffd3caea5a0677d60b493d1813767f4bcd788fa7","datavalue":{"value":"7189663","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1987736$642C458E-04AF-418E-B45C-BE09ACCC9DE0","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e29a0a1a089c1739ef594b8aa170de0991ebf7f7","datavalue":{"value":"proof checker","type":"string"},"datatype":"string"},"type":"statement","id":"Q1987736$9C3E6593-EF9B-4200-BAF5-335F48847C78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1987736$5E150A12-9D9B-4EF7-88C3-286342437B14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ed5b36acbbcdd78ff381b3635ec25a20340482b","datavalue":{"value":"mechanized proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q1987736$473D8784-E0E2-47F8-8557-7FD51F119918","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fe51228e17b836f3520db7bc0de40e5086eebee3","datavalue":{"value":"soundness","type":"string"},"datatype":"string"},"type":"statement","id":"Q1987736$EDE9A9C1-5093-4F7A-9756-8D293A826645","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"801a319db4682ef4442b12d14dec7cb54b5357be","datavalue":{"value":{"entity-type":"item","numeric-id":44336,"id":"Q44336"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1987736$B72E9FC0-AAF1-4B48-9A6D-2033A31221BB","rank":"normal"},{"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":"Q1987736$2F53427D-FC4C-45E4-B2F9-C6E4959036A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"533959f24a509b955614f607e46b8aa4cec190ef","datavalue":{"value":{"entity-type":"item","numeric-id":20799,"id":"Q20799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1987736$CDABE2CF-8948-46BE-9587-38A47FDB979E","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":"Q1987736$FDFF1A36-5F61-425A-A2D8-1A2BFD5D23DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"73bf07fb0985efe0166024eb806e5cf2244671a5","datavalue":{"value":{"entity-type":"item","numeric-id":18489,"id":"Q18489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1987736$4B015096-3495-46ED-B8CF-B251D218E364","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":"Q1987736$7853C1E1-630E-4956-BAF5-9AAC7255E91B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8820312195fedfa211b44ae20ae12e4a82ec2682","datavalue":{"value":{"entity-type":"item","numeric-id":23299,"id":"Q23299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1987736$CB52F6A6-4B09-461C-BF7E-3F4DE24A2C3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4f930b95045a1000563a1c7315d8b3659e0c990e","datavalue":{"value":{"entity-type":"item","numeric-id":26832,"id":"Q26832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1987736$83B5A053-708A-4D19-A500-2BE831110AFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8b2040a476017b43b21bd352cfec0a67d631d6d4","datavalue":{"value":{"entity-type":"item","numeric-id":18467,"id":"Q18467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1987736$C177D00E-354A-4F94-B18F-4D2425A3C51E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e079f4640d565f0ca1930fd327c2c7e8d634508","datavalue":{"value":{"entity-type":"item","numeric-id":21954,"id":"Q21954"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1987736$01D2AC5A-3A47-4F05-A5C3-C607F6D81623","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"44e192ea0614ca90dcab29c306f09db708056c50","datavalue":{"value":{"entity-type":"item","numeric-id":24736,"id":"Q24736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1987736$015280CC-11E8-4CDD-BDE4-E8D13BF277C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"468fad61234030d4d4bd64e4991e6e30fb2af1d0","datavalue":{"value":{"entity-type":"item","numeric-id":29451,"id":"Q29451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1987736$FBC357AD-82EA-4A9E-B638-F027F24A1019","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":"Q1987736$32A79B7C-7ED1-4926-9642-A7EEFE8AADF9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"01607eab00ed1b3fb1dff602d0139134c07c390a","datavalue":{"value":"https://doi.org/10.1016/j.jlamp.2020.100530","type":"string"},"datatype":"url"},"type":"statement","id":"Q1987736$AFFA85CD-4D3E-4619-9BFD-6F518D19A4B3","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"fdbc9761b433f572c16fe6d13b5b049aa9d4e9c2","datavalue":{"value":"W3007423032","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1987736$88783C9B-1EBA-43B9-96DB-64DBF87A6447","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"92281f917da3a00fe0192413035ae6a90371a0b1","datavalue":{"value":{"entity-type":"item","numeric-id":287361,"id":"Q287361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1987736$5CD57FF9-44E9-47E1-9136-680AF90AC8BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77f4334b25d43b9293350a877e2d317280ca55a9","datavalue":{"value":{"entity-type":"item","numeric-id":3543646,"id":"Q3543646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1987736$1BCD74B2-BD21-49C9-AAB4-E7C97845BC9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"46bace28fbebf820c63fed72ed21b2a304c9cac3","datavalue":{"value":{"entity-type":"item","numeric-id":1799129,"id":"Q1799129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1987736$A5AB7C17-03C0-4768-8CE6-E58EEC52B23B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3d93e889c52c36a6fb58e10f9eb9b5078b5353ce","datavalue":{"value":{"entity-type":"item","numeric-id":4972072,"id":"Q4972072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1987736$471A8CC1-BB90-46BE-8D37-77BBB5923691","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"17a69741364102658aa60a87b94db8d7506ce725","datavalue":{"value":{"entity-type":"item","numeric-id":3183517,"id":"Q3183517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1987736$1544B6E2-82B3-4425-ADF1-7EA7A5BC7146","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aeedc506ee95714a79cfc16f82862182df8774bc","datavalue":{"value":{"entity-type":"item","numeric-id":3613408,"id":"Q3613408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1987736$AAE52D93-FF77-4D15-860E-16FB71176B1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"567a8dff2d0b10b014f06f4bbf8ecdbec1e09916","datavalue":{"value":{"entity-type":"item","numeric-id":2988660,"id":"Q2988660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1987736$18E3DB82-BFF3-442F-A206-B974AB730817","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6d1e46bde366c9665559a7c22a84b5c9d3a328b4","datavalue":{"value":{"entity-type":"item","numeric-id":5408415,"id":"Q5408415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1987736$E0143AF7-74AF-4F03-946E-1413F58B2F7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"58b883d872eefbd5f8daf82a38b9e66e81e1a15c","datavalue":{"value":{"entity-type":"item","numeric-id":5477663,"id":"Q5477663"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1987736$CA460454-0D7B-4D17-92D7-CA228F2E6190","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1987736$4066DA3A-3F2B-41AD-AA22-3BF68DD6A336","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fcd44752aa5df5cd038054d2d30c6001d6392b03","datavalue":{"value":{"entity-type":"item","numeric-id":286790,"id":"Q286790"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1987736$E6D39DAE-7531-4A10-86AC-11412FBFDF27","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"18e1b4e7833dfe6e6435211201a769e28cc98521","datavalue":{"value":"10.1016/J.JLAMP.2020.100530","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1987736$DD12A8AD-D4AC-4B3B-AE3C-67657A3420F6","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ed8aba500f89cbf727442fbde664c82a20d58a91","datavalue":{"value":{"entity-type":"item","numeric-id":2108191,"id":"Q2108191"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dc73b0cd32bfc624fbe69099e4f20691321fbfab","datavalue":{"value":{"amount":"+0.7745541930198669","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":"Q1987736$966015B7-9DA2-4103-882D-0F5A1F221995","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5ca6b33a9f213e3f67729583300a9e1f98b54e7d","datavalue":{"value":{"entity-type":"item","numeric-id":287361,"id":"Q287361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"738f7398e7d13c8c5f024e21b0d26203be5f624c","datavalue":{"value":{"amount":"+0.7497882843017578","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":"Q1987736$E834B6D0-4EB6-49AF-9C94-9DC440BDA6F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1335255e53437e5ef4f817148c595db6c02a4ba8","datavalue":{"value":{"entity-type":"item","numeric-id":3024890,"id":"Q3024890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3258336ba6cb2824e76b71ccebd56032f976856a","datavalue":{"value":{"amount":"+0.7492526769638062","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":"Q1987736$8E160F74-3674-42DF-89A8-CA811DC1A46E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"534ab4cc528829f573af9e6705220481f24ef1c0","datavalue":{"value":{"entity-type":"item","numeric-id":5168887,"id":"Q5168887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a1fb68412cb6ef1449a420c01d7567a49c6430b4","datavalue":{"value":{"amount":"+0.748218297958374","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":"Q1987736$10E59541-003F-4598-BB21-CB1CCC9DE680","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"61e2a43b4930e1e1440ed8b96c6f962cc673db8c","datavalue":{"value":{"entity-type":"item","numeric-id":2829278,"id":"Q2829278"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7a1a8119f5b312eb7df606872a0e8546e36a9fe6","datavalue":{"value":{"amount":"+0.7422814965248108","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":"Q1987736$EBDF5B14-C16D-4687-B313-AFC2BB7979B2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1987736","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1987736"}}}}}