{"entities":{"Q287356":{"pageid":289123,"ns":120,"title":"Item:Q287356","lastrevid":60719007,"modified":"2026-04-10T18:42:58Z","type":"item","id":"Q287356","labels":{"en":{"language":"en","value":"Interactive theorem proving. Preface of the special issue"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6585631"}},"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":"Q287356$56132382-BCB6-4221-AC42-3FCA6A5EFFD0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b5a1152a8ccfdccc337647db4ab2f518c9602327","datavalue":{"value":{"text":"Interactive theorem proving. Preface of the special issue","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q287356$96C361C4-B2AE-44BD-BC6C-D58A80699298","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d779e9f9be95ecb4d6a880ea1b57e907a64f66c3","datavalue":{"value":"1336.00112","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287356$34CFA8DC-4C96-4484-86F4-571874072F2F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287356$D91BA246-98CA-4B5E-BFA6-520E526D85DF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b626bb78b3e93b3076e6958296f7f25e2e74c3ab","datavalue":{"value":{"time":"+2016-05-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q287356$C1B5F576-3EB8-46EC-995E-46A0CD8EF553","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"342a6161f41187e2c595daa41b09cee10ab1ace9","datavalue":{"value":"00B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287356$83713266-7C11-42A1-99A0-E4E0A0333CA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed293b811733fa9438a72e1b6ba5680a0d2aac9e","datavalue":{"value":"68-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287356$419A1086-30D9-410C-9BF8-3A16E26A6BAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287356$5E90ECB2-DABD-4E25-A25D-63B712EDFD44","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8fc31e0b9a549133637fd87c1b5ca3e3b4fea522","datavalue":{"value":"6585631","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287356$D4FCE6E1-3D9E-44C5-B1DF-782F399989AC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q287356$0C52D3C0-0C6A-40C3-B101-3A18B68E266E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q287356$D507C6A0-8473-46E7-B0CE-E4DC8D4DB0E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cd6f648bd1eeb66cc548d9608d64c3a3e1ea7e29","datavalue":{"value":"formal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q287356$6F39DB5C-D678-430F-995A-EFA186A081C8","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287356$1570C23F-DD95-4914-A338-860A1BFEEF58","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":"Q287356$6D101F3A-C7B1-4F17-8396-342EFA45ACF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c2e87d897ce5d80b030b7930ad6e7942edbeeaaf","datavalue":{"value":{"entity-type":"item","numeric-id":24996,"id":"Q24996"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287356$C259A385-774A-4A92-8C0C-141C8E962037","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a94daa7865c51c0d2412cced8422ea9361d06e30","datavalue":{"value":{"entity-type":"item","numeric-id":21343,"id":"Q21343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287356$AE92FF4F-2E32-46D2-B4EB-F40B4C43C1AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287356$C13F5420-0E47-4F44-9B00-2777EB6208E5","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":"Q287356$2D926C5C-133E-4BE1-BA41-E5EF700FC0EF","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":"Q287356$C69E2101-9437-4EA4-8324-3F7C931218EE","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"71f8f5e90d76e5a2c543a204b196b921dad05b2a","datavalue":{"value":"https://doi.org/10.1007/s10817-016-9363-7","type":"string"},"datatype":"url"},"type":"statement","id":"Q287356$D4E605FF-7B5E-4CA4-A11C-99C1A60AA04E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0a4ead4ede2c30b62d1f1bb18a452d6ae533439e","datavalue":{"value":"W2284603212","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287356$829BF1C6-5017-4A78-A3F2-20A32421E910","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4b474ecb2c93cbdc37aebc22b5ddf0b796b0b587","datavalue":{"value":"10.1007/S10817-016-9363-7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287356$9A4CDBB9-AEF2-453D-8BBC-C82714C6BEC5","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6b5cd105b44770aa835c9cbc85b4fcf5656f16d0","datavalue":{"value":{"entity-type":"item","numeric-id":5894305,"id":"Q5894305"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"81948a605aa4951603c2b1b65da0788228efcdac","datavalue":{"value":{"amount":"+0.9704585","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":"Q287356$EB29E1DC-9AB4-4153-8304-A0DB3746D022","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c32f2cbb8a453222b98cdf0e974734e0b4ea4a11","datavalue":{"value":{"entity-type":"item","numeric-id":5094469,"id":"Q5094469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6e0445728a8c584bf6f24d18b7937827677df4e2","datavalue":{"value":{"amount":"+0.9647076","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":"Q287356$39013C05-D64E-4741-B96D-760D360B9181","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b5a66faa01dbce681557a69b916ebefc9578b7e4","datavalue":{"value":{"entity-type":"item","numeric-id":6173578,"id":"Q6173578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"876565fd1b9e15e651f26efb3d09c3cdde03fda1","datavalue":{"value":{"amount":"+0.9437678","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":"Q287356$405F9421-98E7-40FB-B901-058F4357A5F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9a3c074ee182c14fb829f48d8ee3067fb50232e8","datavalue":{"value":{"entity-type":"item","numeric-id":3336730,"id":"Q3336730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1a3f9c54353479b482d6ffc505a4951bdad803b2","datavalue":{"value":{"amount":"+0.92917377","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":"Q287356$2B7D2645-6295-4300-8086-4B10E1E02FFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9a02b2bfea1c5f47cd601f5ce8d9525ee86d87fe","datavalue":{"value":{"entity-type":"item","numeric-id":5219926,"id":"Q5219926"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0f2cb5b922ca46e4eb67a45e60950496857caade","datavalue":{"value":{"amount":"+0.91541684","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":"Q287356$103211EA-2CF8-4438-A3C1-4A2397DAF2DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0b334918dd1a2aa0f0f022268f87ecb12c10c047","datavalue":{"value":{"entity-type":"item","numeric-id":2881098,"id":"Q2881098"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a9527e2c51e99fd9d8328469cfb412157cca8174","datavalue":{"value":{"amount":"+0.91425335","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":"Q287356$7FD4C371-1640-418C-8BD0-E95969B76F49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"14390bb381c2466373902e6a7612c72c7a54f6ee","datavalue":{"value":{"entity-type":"item","numeric-id":5741556,"id":"Q5741556"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5d0b4cca45e0d6cd039c48077feded3cfc176a29","datavalue":{"value":{"amount":"+0.8988509","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":"Q287356$FE8F8FE9-77FC-4292-8D9C-7BA65C3D5B51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9726cc7376f9c9e17be44376106ad9280d3b83e4","datavalue":{"value":{"entity-type":"item","numeric-id":2819200,"id":"Q2819200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9945e9629129deb125fc5c8da3af1eb56402f3bb","datavalue":{"value":{"amount":"+0.897727","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":"Q287356$ABE4B60F-51ED-423A-9A6C-36EFF87C325C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b028676b8970ef098bbbc9e5238ddb908899ecbe","datavalue":{"value":{"entity-type":"item","numeric-id":1353946,"id":"Q1353946"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c00310acae63bff56dd1ec63b966545af52d0cb5","datavalue":{"value":{"amount":"+0.89729095","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":"Q287356$24E5C067-55E8-4AB9-B29C-386E19C111DB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Interactive theorem proving. Preface of the special issue","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Interactive_theorem_proving._Preface_of_the_special_issue"}}}}}