{"entities":{"Q5287513":{"pageid":7317087,"ns":120,"title":"Item:Q5287513","lastrevid":46349664,"modified":"2025-12-24T15:06:32Z","type":"item","id":"Q5287513","labels":{},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 234014"}},"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":"Q5287513$33F2ADDA-5872-442D-8B68-AC7304C1327D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c6b2488e34add6e9bae41687c415d24936e60a18","datavalue":{"value":"0779.68007","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5287513$1704BD98-50F9-4950-854A-06C46E5411DF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"60a6cc2906ab33f788af6d51cf03c39f0d4046ba","datavalue":{"value":{"time":"+1993-07-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5287513$7AC9034E-F026-43DD-80CC-107FFBDE343F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed293b811733fa9438a72e1b6ba5680a0d2aac9e","datavalue":{"value":"68-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5287513$7691C2B5-CD07-4C2C-8AE1-9D31FB7CB55B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5287513$49148FA6-E055-4DA2-869D-8F8A63E2149E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"71887e6a70355ca3c55c3d2bb6b6b85e5351c5d1","datavalue":{"value":"234014","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5287513$2FBFFA46-F6D0-4530-B7D9-C78D61C1DA01","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5343ecd15a8e87cb138c7d9e4c8f0d52a5afdb65","datavalue":{"value":"HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q5287513$5FB5FB42-582D-4630-878B-9166B195B64A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"01873808ed420453ae082d7e18447e172733687b","datavalue":{"value":"higher order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5287513$C4E83116-E138-4546-860B-9FA2707D517A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5287513$9EC9C89C-0540-4C95-9E0C-69C5D1B351CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f43e3c61c91c261829262bd43c262e68558b5743","datavalue":{"value":"verification systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q5287513$7B42B993-E90D-4BD7-9D83-1B8A3C6FE456","rank":"normal"}],"P1463":[{"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":"Q5287513$466BBE8D-9F44-4363-AF77-0B6478BAC037","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":"Q5287513$D19C09DA-91FE-4315-A4F4-2B8C62298F34","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9d8c676f8538b024eb2a80be0edde23296e2c1db","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"525425ac5e35068867df3ab9290a01f01d85441e","datavalue":{"value":{"amount":"+0.8230403065681458","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":"Q5287513$2314C459-21C3-4F6F-9CC4-3C977926914D","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":"26936d186b7ccac8d63fddc3fc0ea9abfa4b4cfd","datavalue":{"value":{"amount":"+0.8045547008514404","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":"Q5287513$442688B1-1194-4D95-AD05-212610D3B825","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"efd8dc0e0b76d191fd26f35e8e5741833044fd26","datavalue":{"value":{"entity-type":"item","numeric-id":3543646,"id":"Q3543646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"23041a987aaba48aee72cd7fcd3ba89455353cab","datavalue":{"value":{"amount":"+0.7822325825691223","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":"Q5287513$51A6C3A4-2605-4204-BC90-E151A4C2E2D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"799a38e83bea9921db7a769536fd5def8b656e78","datavalue":{"value":{"entity-type":"item","numeric-id":1923825,"id":"Q1923825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"248e5be74ae6566adbe87c390f439f92729d24b8","datavalue":{"value":{"amount":"+0.7816759347915649","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":"Q5287513$4EAB48C4-958A-4B07-83CE-EBFCD5206917","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5287513","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5287513"}}}}}