{"entities":{"Q3613409":{"pageid":5643315,"ns":120,"title":"Item:Q3613409","lastrevid":50603738,"modified":"2026-01-14T13:14:11Z","type":"item","id":"Q3613409","labels":{"en":{"language":"en","value":"An Interpretation of Isabelle/HOL in HOL Light"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5528287"}},"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":"Q3613409$97A126A8-7EF1-459F-BF27-FE9A67FFD331","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cd2f777fadaf194a09efefe1ebeec86432d9bbee","datavalue":{"value":{"text":"An Interpretation of Isabelle/HOL in HOL Light","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3613409$79AFEB13-BAF4-41C8-A357-E955F3BFDC4B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"511d8f56f4db85b8d4b64c246eb86d62302ec1f6","datavalue":{"value":"1222.68370","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3613409$6BD2EA91-7512-457F-98B0-779AECA1FEF9","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3455fa432fda40f077282952ba9ced2c2efec616","datavalue":{"value":"10.1007/11814771_18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3613409$EA2A4E76-D24E-477D-8619-E86B46BD3BF2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"77ef26b195160569d7e65188fa689f9dd610af9e","datavalue":{"value":{"entity-type":"item","numeric-id":2225087,"id":"Q2225087"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3613409$95468E5F-B389-4A4F-96C4-FEEE8D23F146","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3085facee3457e7f15d7356906b0165b8709b141","datavalue":{"value":{"entity-type":"item","numeric-id":2817907,"id":"Q2817907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3613409$64AFDE31-6F0A-4E8F-AC47-78703ADAF000","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5633353462eee310c4db3234ed97ea2c49f28694","datavalue":{"value":{"time":"+2009-03-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":"Q3613409$9AD9DFF1-8023-42C8-8EFE-A31F751D5F12","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3613409$6350837E-944B-44AB-8536-A1BBD6786DFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3613409$EE2B65DF-DA7A-4AF6-AF90-FEEBBA7A6995","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a866621b96f867671f7ef0818c1038c8bfe951be","datavalue":{"value":"5528287","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3613409$FA4BD450-E101-4149-B4EC-CA63DADACC49","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":"Q3613409$4C61CBA7-D277-4901-83E3-8C6A30203C6D","rank":"normal"},{"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":"Q3613409$251D23F6-4631-474C-B346-3AE7001DFA5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"73bf07fb0985efe0166024eb806e5cf2244671a5","datavalue":{"value":{"entity-type":"item","numeric-id":18489,"id":"Q18489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3613409$AA4FBCBE-6EC6-4F68-A43E-00D4734DC833","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"040fe209bf9959da562393c0e37eb31592733af3","datavalue":{"value":{"entity-type":"item","numeric-id":18957,"id":"Q18957"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3613409$FC119DEB-4B9B-4E9C-A9BC-3BCB998E6376","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":"Q3613409$627BBBA2-DDBA-46A5-98B3-19594FC0E687","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":"Q3613409$7D0DACC9-5AFF-4DE6-B77F-CDCC80AB0BE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"27b6ae20da44d6f09b655d9481cc0df08a8ffcdf","datavalue":{"value":{"entity-type":"item","numeric-id":18826,"id":"Q18826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3613409$4508BAAB-905F-464D-8BB6-EF3A9B2FD39E","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":"Q3613409$26182095-91E5-443C-8EB8-C2B8B44F5942","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c9dbc3fe1320bf88348f798524e0a5bf7f839047","datavalue":{"value":"https://doi.org/10.1007/11814771_18","type":"string"},"datatype":"url"},"type":"statement","id":"Q3613409$6BDA4C53-FE41-4B68-BE02-9B79996CEC6B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5b9eb9d4401005b20d5ca352659484d2a286da32","datavalue":{"value":"W1488510713","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3613409$707C68A3-03FC-4365-9307-C3B4C32C0A80","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"939cd2c4229824b8a14b7f16dc661ddbc20c89e4","datavalue":{"value":{"entity-type":"item","numeric-id":5747657,"id":"Q5747657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4420c6ae731bf142a696bb718341ca56c375a0af","datavalue":{"value":{"amount":"+0.7888257503509521","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":"Q3613409$2722C561-EB25-44C8-9935-344951315C6A","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":"e46fbdea57700d38b496d85640971f5b803e48ad","datavalue":{"value":{"amount":"+0.7850067019462585","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":"Q3613409$9A3B6E4B-6A1F-45CA-BDB5-80E1B50FA9D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ef914c5d16ae991870856bd539a5283395a477b7","datavalue":{"value":{"entity-type":"item","numeric-id":3543647,"id":"Q3543647"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b78becc9b05114ecd819f11f5151f70590545436","datavalue":{"value":{"amount":"+0.7657809257507324","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":"Q3613409$4462E1B6-E06C-4729-909F-4E56A4EEAC59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f1cab783396284eb004b42756f108087b79277b8","datavalue":{"value":{"entity-type":"item","numeric-id":3613408,"id":"Q3613408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8a010dbad963cc5c8faba7291b8130ba5659bb19","datavalue":{"value":{"amount":"+0.7572899460792542","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":"Q3613409$6B37BACE-79CF-4570-8F5E-BC9E369A0DD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5a89dd6970994c099e3030bbed6db81931530f4a","datavalue":{"value":{"entity-type":"item","numeric-id":5747659,"id":"Q5747659"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"659fc7c4d7bf2fbdd52ceb52eb9459f9d25a9e48","datavalue":{"value":{"amount":"+0.7559054493904114","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":"Q3613409$9E2CF32E-BEEB-4A94-B9D7-009B2858F3AF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3613409","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3613409"}}}}}