{"entities":{"Q4231030":{"pageid":6260631,"ns":120,"title":"Item:Q4231030","lastrevid":46615029,"modified":"2025-12-25T05:36:04Z","type":"item","id":"Q4231030","labels":{},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1259143"}},"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":"Q4231030$3C718AEA-1AD9-4D2C-964A-796FE250E788","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5a577ed17d5bf771af95ce05771ec772e0a321a9","datavalue":{"value":"0932.68099","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4231030$E22B8BD2-6CC5-4702-A372-37263473BA0F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"eeb380f564c5a8f0fcd332fa7514de56929165f6","datavalue":{"value":{"time":"+1999-03-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":"Q4231030$51AB8605-EEFE-4718-8FD4-93B2AEAAFFFA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4231030$47515F39-693C-4333-B446-3ECD0E26B293","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"98c5206e338942c77451c20a9a5ffe8ae1a4cf18","datavalue":{"value":"68-01","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4231030$D77F337A-93F6-4DF5-BA14-1624264AA3B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4231030$42FFE813-F155-4887-A563-F2E2AF0AB5B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6be78f1bad1f2f19058dbde65eb124c0430a7d27","datavalue":{"value":"68W30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4231030$66743C49-DA7C-4DC1-B50E-F325886B61C3","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"27d1d585e8054c9c11101f80ab91f17d3e761b8b","datavalue":{"value":"1259143","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4231030$B9541A4C-D2C7-438D-BB02-E96FD8D2D39B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7c2a9a0ee15dbb4bfd89047300f0dab1f2cb4127","datavalue":{"value":"HOL theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q4231030$0131E224-8E76-4737-8250-11CDA07AB507","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6f632f4e0a5cfab23758463f1559679989e4a63a","datavalue":{"value":"floating point","type":"string"},"datatype":"string"},"type":"statement","id":"Q4231030$047166DD-4F7C-49B8-89DF-72EACD181152","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4231030$4074FEF0-3935-4DC6-884B-9FD5F734FE6A","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":"Q4231030$4B853BFD-3CE6-4C37-9E35-1354C26526D3","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"52785f2dd2003261c737010c9dd8c0d12eaa464a","datavalue":{"value":{"entity-type":"item","numeric-id":1334896,"id":"Q1334896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"38391de1470f52a9759bcafd29d3ddd2bf883faa","datavalue":{"value":{"amount":"+0.8776960968971252","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":"Q4231030$7FBBA76A-3A38-43C9-B913-75DCB0DF1A55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bd7be6caaaa2c317c345966210e02cb9b65737f9","datavalue":{"value":{"entity-type":"item","numeric-id":2973239,"id":"Q2973239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2e493df35e76a55cad01ffe66c05c2fb18beb246","datavalue":{"value":{"amount":"+0.808854877948761","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":"Q4231030$2A643A99-CFE0-49C2-92D6-2F56BBC07E69","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"24c4e1af29df48aba6865efb69804492ca54b4af","datavalue":{"value":{"entity-type":"item","numeric-id":2703760,"id":"Q2703760"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"645d07263256aea96e7da483efe858b9df3d56ab","datavalue":{"value":{"amount":"+0.8084201216697693","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":"Q4231030$E186ACB7-9D98-4237-8BAF-B70516F74843","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5d4a936d98ae0d5ebdcb9122e43f543841b8a600","datavalue":{"value":{"entity-type":"item","numeric-id":4594262,"id":"Q4594262"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"90584555ab310b1e608c6bdc5891834e68c2846e","datavalue":{"value":{"amount":"+0.8045210242271423","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":"Q4231030$052BA503-AFDB-4A9C-A116-87AC8EBD2BBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8648fefe25b990ca49378b9d175a37f95f66e4e9","datavalue":{"value":{"entity-type":"item","numeric-id":3543660,"id":"Q3543660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6e40133e08fd1d4167dec4cb78902bf1d400fb95","datavalue":{"value":{"amount":"+0.7961217761039734","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":"Q4231030$969C628F-9512-4B02-9FD1-93FBA3A60DB9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4231030","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4231030"}}}}}