{"entities":{"Q1600086":{"pageid":1610826,"ns":120,"title":"Item:Q1600086","lastrevid":71397420,"modified":"2026-04-13T22:00:39Z","type":"item","id":"Q1600086","labels":{"en":{"language":"en","value":"Isabelle/HOL. A proof assistant for higher-order logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1754490"}},"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":"Q1600086$3E3026A7-8BE7-448F-88E4-0AEA7CD1E558","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cf35577a28512058886e2c7a71a5a86dc9e3209d","datavalue":{"value":{"text":"Isabelle/HOL. A proof assistant for higher-order logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1600086$AD08AA95-6B6B-4EE3-9BEB-9B93CCF4B07D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"aeb473c5e6fb43f73cee5de8f2fd9f7044d7a2eb","datavalue":{"value":"0994.68131","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1600086$763277A3-4505-4EFB-87EF-DB48C1A03EF8","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"bd39997decddd4925a8ef09cbbffc4f41d2b1f00","datavalue":{"value":{"entity-type":"item","numeric-id":670700,"id":"Q670700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1600086$34A048C7-1A2F-4636-A861-BB07711FD260","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"877cdd48b78659fb34c7540ccd4a9d80f4f6eaf8","datavalue":{"value":{"entity-type":"item","numeric-id":1600085,"id":"Q1600085"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1600086$55CF73CB-EA39-427D-9DB4-9155A0CE19A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"cb5dfbdfa6d8a2070a67ff948fb8abd387eda36e","datavalue":{"value":{"entity-type":"item","numeric-id":352969,"id":"Q352969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1600086$C148C8F5-675A-4858-AB33-196CFE89884B","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":"Q1600086$F3CE1D44-AC43-43A2-8E3F-B9C5E083DB9F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"61236299fa791b99e4b27b6369e8c14dcf94677d","datavalue":{"value":{"time":"+2002-06-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1600086$B504C98B-A559-44EC-BBEB-697879E1385B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1600086$D97EF38D-AEDF-4810-8E1F-85F834F66EE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"24aafcf24a21bd70cd3b62d3f5f72a6d0d82d816","datavalue":{"value":"68-02","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1600086$3EC8543C-B174-4A0D-98E9-433682130CD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1600086$F53DE089-49DC-49D3-949C-54B5D8F4A1BE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a4aec33384c39cd6fd6e10f23c84156bc3ad5d12","datavalue":{"value":"1754490","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1600086$C4DCB0AE-2E66-400A-AE05-63CD0840763A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7eefb2b1f5e1ddd95f5db204b23cfb4c53d0151","datavalue":{"value":"Isabelle","type":"string"},"datatype":"string"},"type":"statement","id":"Q1600086$890F0F77-50F8-45B0-9A9D-5D686305BE1B","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"067e00213990a6f2431e78667be3f10443c92f4f","datavalue":{"value":{"entity-type":"item","numeric-id":16052,"id":"Q16052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1600086$A03CCAB2-12CA-4D2A-9DFF-0FC570C2104B","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":"Q1600086$A9EA768D-9AF8-4CE7-B937-4B2F6EF6D614","rank":"normal"},{"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":"Q1600086$EA9F8A21-4C56-4B7E-800E-FB7F63C10F73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9aeef25d5839625565921d83cf1c652bf6f2fbf6","datavalue":{"value":{"entity-type":"item","numeric-id":17052,"id":"Q17052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1600086$3BA4BA29-39C1-4C33-8824-EFA0FC72C93C","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":"Q1600086$5E1810C8-D008-4DBA-AD91-3A6A140186C2","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":"Q1600086$55833D1C-DE18-4400-9158-A2DD084861D5","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8fd5c2832aabbf4b304824c9b3020a0ed9253b4e","datavalue":{"value":{"entity-type":"item","numeric-id":4823141,"id":"Q4823141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"266ec0348bf7ca2865abc64690d4646376538024","datavalue":{"value":{"amount":"+0.9340358","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":"Q1600086$8960D89A-C9CB-4E21-9EDB-A6B8AE69FFE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b0a588c992f66473ce2128ef7f91aa58bc970e2d","datavalue":{"value":{"entity-type":"item","numeric-id":5145439,"id":"Q5145439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"83c3d75aa293744aefdd2ec90c450a8fa4f6ffc3","datavalue":{"value":{"amount":"+0.919202","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":"Q1600086$6037827B-6F71-4035-810D-4994AC2529D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cef7c286fb322135f98a489f42e729b7284efa24","datavalue":{"value":{"entity-type":"item","numeric-id":5287513,"id":"Q5287513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"db01849bd5f7ae30e59ad4409494cf9e209c2f0c","datavalue":{"value":{"amount":"+0.9185866","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":"Q1600086$1CAC6DFC-523B-47A8-A436-6DB5FA98DCB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9ca334c71b2f31093563b1df55327e8a824bfeca","datavalue":{"value":{"entity-type":"item","numeric-id":5415649,"id":"Q5415649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"20dc99fcf124b60676b979c73392948daec7ba9b","datavalue":{"value":{"amount":"+0.91749126","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":"Q1600086$29472DA4-8DE0-4C52-A252-400E6F87E580","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e1aac3c3e28f3c5c8a5eba2ddfcb1c23067c2156","datavalue":{"value":{"entity-type":"item","numeric-id":2405272,"id":"Q2405272"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"82030fd45d90ff4b6af2373844ead93790f97d44","datavalue":{"value":{"amount":"+0.91412544","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":"Q1600086$195E06CE-E2E8-4A55-919B-B0EF9B5ED992","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"353f83759ee34b781b1cadc49c3f90042799760c","datavalue":{"value":{"entity-type":"item","numeric-id":5200122,"id":"Q5200122"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"39d25de801ecac1133433399d41cdca0b80ebdd4","datavalue":{"value":{"amount":"+0.9087141","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":"Q1600086$126CB0E4-E354-4520-B461-5993DBD0FF64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c4d6a02e8ed4be52df77c85be2c6cec6b5104aed","datavalue":{"value":{"entity-type":"item","numeric-id":6159365,"id":"Q6159365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9f74dcf7d9997b69551a4c68303e477a66f8c5be","datavalue":{"value":{"amount":"+0.9073596","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":"Q1600086$013512F9-626F-48C8-931D-F91F6D157FFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"38394b4e8d3a3502630a463829cd1f4840ac5524","datavalue":{"value":{"entity-type":"item","numeric-id":3172879,"id":"Q3172879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"49a7bac8117d32e57472f60297087b604e3d67d2","datavalue":{"value":{"amount":"+0.90605676","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":"Q1600086$66B4FCD3-732A-4B64-8ED4-26373697B87E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9b4bd063345fb4a33e51cc534c9c83293f893191","datavalue":{"value":{"entity-type":"item","numeric-id":2128791,"id":"Q2128791"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c1d4ebc13797ab3b2d3bae44fd87546547f06494","datavalue":{"value":{"amount":"+0.90528536","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":"Q1600086$2490955F-08EA-4EC0-B02D-25109963835D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f007afffaa9d82c697dfde08e38474d46ab399f3","datavalue":{"value":{"entity-type":"item","numeric-id":1739913,"id":"Q1739913"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fa6a442b195fc28f7fb021b6afce329b087d5791","datavalue":{"value":{"amount":"+0.90316635","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":"Q1600086$98540FD3-9446-4999-A6C1-F2C6CD88720A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Isabelle/HOL. A proof assistant for higher-order logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Isabelle/HOL._A_proof_assistant_for_higher-order_logic"}}}}}