{"entities":{"Q2055899":{"pageid":2066641,"ns":120,"title":"Item:Q2055899","lastrevid":57686859,"modified":"2026-03-31T22:09:23Z","type":"item","id":"Q2055899","labels":{"en":{"language":"en","value":"The Isabelle/Naproche natural language proof assistant"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7437104"}},"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":"Q2055899$01E827BB-B84B-43D6-A9C3-A81660F12515","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1400f4973ce755ba04bd7b785e50d08fbc4c2f8a","datavalue":{"value":{"text":"The Isabelle/Naproche natural language proof assistant","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2055899$7214D965-77F9-483C-B9B0-5F61CD77A975","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2a6d2fb10bcbd2512e2da2494f7f02f26294248e","datavalue":{"value":"10.1007/978-3-030-79876-5_36","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2055899$85327DC7-3493-4D54-9460-C3743DA13312","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6e5ef3c09dbe743228f36a4d9b380063a6dc6203","datavalue":{"value":{"entity-type":"item","numeric-id":2055895,"id":"Q2055895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2055899$CBC12363-13DD-4994-A9AF-22AAF56959B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"97d0b9b61d83d1e98f6242a5df0440e02577e539","datavalue":{"value":{"entity-type":"item","numeric-id":375822,"id":"Q375822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2055899$C54FA59E-0D38-43F8-8D9C-92B1E69F4ED0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"87159b4f68d14237460a9d9df76f5a804b76cde2","datavalue":{"value":{"entity-type":"item","numeric-id":2055896,"id":"Q2055896"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2055899$6A069066-49FB-4C10-9339-3E6F00A291FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"cc28df9555a9803a43ddbbec457bb58b52f60ca9","datavalue":{"value":{"entity-type":"item","numeric-id":2055897,"id":"Q2055897"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2055899$98308DE3-A168-49FE-B1E4-0233BD50E5F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1739a6cc2bec4304864e33cc6d227647838111a1","datavalue":{"value":{"entity-type":"item","numeric-id":2055898,"id":"Q2055898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2055899$C7468AC8-1A84-4F64-9A67-2E9F6212E078","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a162d67ca0f0da05fadb758011f7efa5d1e07db6","datavalue":{"value":{"entity-type":"item","numeric-id":287364,"id":"Q287364"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2055899$2E02B4BA-9777-4AE9-B05D-7156679E5A57","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"083b9dcd5269b8796cca7eb2ababa434dff5de3a","datavalue":{"value":{"time":"+2021-12-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2055899$149C4267-CFA7-4FDD-B59E-34DBE81A7807","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2055899$1428CF1C-0E43-4066-BA60-7E39DD2236CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2055899$C86C02FA-A40A-443F-B57F-AE8EA22A2D20","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a0471aad094b08576dba3996c0d0b43277092899","datavalue":{"value":"7437104","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2055899$370B3764-6B37-4435-B371-D72CAE36862F","rank":"normal"}],"P1463":[{"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":"Q2055899$2EFBD75E-5A8B-4186-9F79-1C64672A5F0E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"dec9660857c05980e3c0b17c51d483bf1a29e419","datavalue":{"value":{"entity-type":"item","numeric-id":40021,"id":"Q40021"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2055899$BEC21DC0-2DD5-4CCB-AAAE-D4F45551C90F","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":"Q2055899$F6D6BBEC-AA20-4820-9E40-0023AA5CBA9F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19c3232540dc15c9350e8393498317de25361cb2","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2055899$8258CA24-6626-46DE-893F-178ED3B8D728","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1017108dce3983431546a14c274f65bc4aaae70b","datavalue":{"value":{"entity-type":"item","numeric-id":22154,"id":"Q22154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2055899$2D049CEC-97D5-4B6E-AF3E-46879CE572F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"211c43a5b835fe620b561d29820fa20ae55def41","datavalue":{"value":{"entity-type":"item","numeric-id":45361,"id":"Q45361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2055899$E88C625F-E679-490F-8195-3F96728686F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b222922e2b373ab7fb2b7a049f9de07c755ee255","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2055899$094D3DD1-5106-4B48-B0B0-1C016598C8AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"91b852acc0d0dcb394ea74c8e76a901ae0257702","datavalue":{"value":{"entity-type":"item","numeric-id":21776,"id":"Q21776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2055899$FFC6794F-CA18-4EA3-8370-E1943C656C96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"39d1d25ae8c00cfad058b188db36fd61dac09925","datavalue":{"value":{"entity-type":"item","numeric-id":27041,"id":"Q27041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2055899$EEFDCE81-2574-4D60-8115-64FCCCEF292C","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":"Q2055899$C82EA48E-AEA5-4A7F-945B-F0933B8008A6","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6fc5f1fee58501460aa9cbc2a77b5c06f6fe32b2","datavalue":{"value":"https://doi.org/10.1007/978-3-030-79876-5_36","type":"string"},"datatype":"url"},"type":"statement","id":"Q2055899$BA34C89E-6BFF-48E6-8828-BCCB79B5741E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e3422a69a13fa80764ce34720ac72a0d0c232a4d","datavalue":{"value":"W3178653101","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2055899$0E2D31D9-F535-440B-927C-6F22284CA19F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3dd33855336399d060e4c0008afb085c9559eabd","datavalue":{"value":{"entity-type":"item","numeric-id":5747782,"id":"Q5747782"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2055899$89E64742-7179-415C-A547-17FE7FAB1784","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"92e8c5efe62c1f0f284e1e3160910ccbd8c92ecf","datavalue":{"value":{"entity-type":"item","numeric-id":2219386,"id":"Q2219386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2055899$B3EFE50A-BD4F-4FC7-BEA0-84655456B2C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e14549321cbae3c57ae9ce6a9266b4af3d64fd4f","datavalue":{"value":{"entity-type":"item","numeric-id":286800,"id":"Q286800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2055899$FA56A072-7108-40C7-9087-9F6CB10639E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8242928870aab67343ad0152eb7ca8357168f7f3","datavalue":{"value":{"entity-type":"item","numeric-id":3454108,"id":"Q3454108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2055899$D8D8E857-BFAD-4795-90F7-E1F626E12B39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4d5de220317fd709a7e63acdecfb92f5c42b492","datavalue":{"value":{"entity-type":"item","numeric-id":2280211,"id":"Q2280211"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2055899$268F082B-5EA8-44A6-B003-037F4C19EB5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93fc8985b7898988b7d52edb5c0cd61c1b917df6","datavalue":{"value":{"entity-type":"item","numeric-id":3150301,"id":"Q3150301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2055899$F74D89E5-FD6A-4FE6-909A-2A3A2A8AC71F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5b79119f9505990ffd9f1c920604fb44a0b0165c","datavalue":{"value":{"entity-type":"item","numeric-id":3608785,"id":"Q3608785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2055899$C1AC9C4E-6015-4079-BF85-354AF35295DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d1dd217b6d60cfd1c7517ad3aa621ccbb5c7c91","datavalue":{"value":{"entity-type":"item","numeric-id":5505538,"id":"Q5505538"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2055899$3A65906A-50A6-438E-A07F-C76337CD0163","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e002a9754659cf7f51ada447f1ca688729d010d2","datavalue":{"value":{"entity-type":"item","numeric-id":2287890,"id":"Q2287890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2055899$F11D15D1-D9C4-4DEE-B988-E8A9CF60911C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"502ad8224b7ee39a96e36cfcfba1b8b740baa8c6","datavalue":{"value":{"entity-type":"item","numeric-id":4790672,"id":"Q4790672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2055899$CD3B236D-361D-4D66-B421-8600DF7BAED0","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"85f5a712434b519e83eb4cd0655faaf4a1e99d17","datavalue":{"value":{"entity-type":"item","numeric-id":2219411,"id":"Q2219411"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9b98d8022e55b4950a2ce379972ccb01c957308c","datavalue":{"value":{"amount":"+0.8579116463661194","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":"Q2055899$1E6D43B2-E187-47C2-AE57-964E7839E51E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6b4b779cac3f7b3f01edcf7c0ad843c1afce2bbc","datavalue":{"value":{"entity-type":"item","numeric-id":2128789,"id":"Q2128789"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c9fe7897b539fedd4fb28eaff3455552be23635c","datavalue":{"value":{"amount":"+0.8554958701133728","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":"Q2055899$B1D83BE1-5F71-4A70-83C0-220AD981775C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"80ba175c3b998324dfef7b31903800589cbb12a9","datavalue":{"value":{"entity-type":"item","numeric-id":2767009,"id":"Q2767009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1406b159ecb265f55a0e65310438065e2396add7","datavalue":{"value":{"amount":"+0.7735790610313416","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":"Q2055899$255F4CC6-06AE-45FB-A2E9-7828338CD807","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e3d791142e1e65a80dacca3a17722b4ad0e5718b","datavalue":{"value":{"entity-type":"item","numeric-id":3696551,"id":"Q3696551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c9989d3f87cc9961d6e06de8f6f2a11acb2eb311","datavalue":{"value":{"amount":"+0.7410717010498047","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":"Q2055899$78DD6C1E-D0F3-431F-AFB7-8909E21E5E90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fffe16400e8645101fc268d3e0a45d194ab4578b","datavalue":{"value":{"entity-type":"item","numeric-id":865648,"id":"Q865648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1ae4056bfcfdbfe5c0eaff98f98544b8de6628d9","datavalue":{"value":{"amount":"+0.7363778352737427","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":"Q2055899$F64BBAEC-3971-45DA-ABD8-B61656ACDA95","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2055899$EB9A24AA-28FC-4FED-AEE4-AAF4B972731A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2055899","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2055899"}}}}}