{"entities":{"Q5387890":{"pageid":7417464,"ns":120,"title":"Item:Q5387890","lastrevid":50366471,"modified":"2026-01-13T21:58:34Z","type":"item","id":"Q5387890","labels":{"en":{"language":"en","value":"An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5279572"}},"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":"Q5387890$57B37967-6895-40F5-8E1B-8067FECE2C3B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"55be8db545cf924d2eeca3741a83618fed2e0203","datavalue":{"value":{"text":"An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5387890$33D93927-B809-4042-A499-07B3CD7BC339","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5cf918791ec8e3c63874e8320ed855590a73c03c","datavalue":{"value":"1165.68473","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5387890$57A3FFE2-2C45-4FF9-A755-DEC01FA35B16","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8d742078b784890c13de07274a9214af0689f4d4","datavalue":{"value":"10.1007/11916277_11","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5387890$36A68A54-4055-49C8-8B9A-5F9337AC617B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6774ae2dfd2eef224a85f98eefe50cc4899b8867","datavalue":{"value":{"entity-type":"item","numeric-id":880986,"id":"Q880986"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5387890$CBBB9D86-6A22-4383-BFF7-E86BFD507F1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e1024ad51fb0c89617301d9b58c1789ce603d4d1","datavalue":{"value":{"entity-type":"item","numeric-id":2092486,"id":"Q2092486"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5387890$6AFCE387-9B43-4A69-B6F6-A3EBF1074A80","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"23864e2be568bb8a6a4b0526f5a5216348320070","datavalue":{"value":{"entity-type":"item","numeric-id":2870110,"id":"Q2870110"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5387890$FFAF3316-2C6C-4999-899E-AB6C7C931045","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6183386ae8366a240584c653ce5ca2494433aedb","datavalue":{"value":{"time":"+2008-05-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5387890$610979F0-1A4D-41DF-9971-43E0498B4BB6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5387890$B624EE79-845D-4D06-99CC-4D91CAF30533","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5387890$63C32692-14E9-4372-8440-8CDB19606491","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5387890$80AE4EB7-EF8A-4B21-9C01-367D4B0A8913","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a860bc5fc2e7fe08f08eb90ecd5d0dbc84eaa914","datavalue":{"value":"5279572","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5387890$9831A8F2-E61F-4A6E-9DF0-0BC140517029","rank":"normal"}],"P1463":[{"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":"Q5387890$5E437931-4084-49F9-8A0D-BADE9FEF887E","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":"Q5387890$772E0792-E4A9-4C7C-8A18-29271BEACF5C","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":"Q5387890$B630B666-5701-4930-89AB-D4E8BC0F4461","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"cbdb3b6ff29f17d8ee30c2a707279aab6fd0d478","datavalue":{"value":"https://doi.org/10.1007/11916277_11","type":"string"},"datatype":"url"},"type":"statement","id":"Q5387890$D3F21D55-EB14-4FEE-87E6-12C74F489940","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"afbe1e0cd9960636e11e259e8ca91dd6e47684a5","datavalue":{"value":"W1523064151","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5387890$552A7CA5-5B10-4DDF-97AD-9E37C07BFE38","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8b7f4e39126d140b1fb7374f494c75cfd56020b6","datavalue":{"value":{"entity-type":"item","numeric-id":4790669,"id":"Q4790669"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e553d8e73b0bebd54aa68df3852a3e60190ecc17","datavalue":{"value":{"amount":"+0.7965533137321472","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":"Q5387890$9B709F28-1A28-4F8C-B8E4-A46D01C24D44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7db5f6f879711fee2556071b86a425c26dd16b51","datavalue":{"value":{"entity-type":"item","numeric-id":3523181,"id":"Q3523181"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1b2e84cbf605402c2ebc0a12ba7e1dbcf929e912","datavalue":{"value":{"amount":"+0.7400137186050415","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":"Q5387890$DF62A151-76E4-4286-BEDC-BE2787F37DCA","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":"24d69e9efb425757605fe543f9e9af9ce7631e21","datavalue":{"value":{"amount":"+0.7318568825721741","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":"Q5387890$5C4E9808-8D9F-47F1-A7B3-960A6F37F789","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d11280eec7f580346c0151d22527bb8d91725392","datavalue":{"value":{"entity-type":"item","numeric-id":2754039,"id":"Q2754039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2cf0f40ba46f61a9352b7e0678604753ce59fd6c","datavalue":{"value":{"amount":"+0.7266943454742432","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":"Q5387890$B3966DC6-8A2A-42B4-8AFD-88AC10A70DEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2740de1b98a7d9aa5a10e33e29be5347f5c1c062","datavalue":{"value":{"entity-type":"item","numeric-id":4375633,"id":"Q4375633"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9d69d842bd7125d7380d4622265723e8d2af034a","datavalue":{"value":{"amount":"+0.7219663858413696","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":"Q5387890$E0EE8390-93BC-4315-A284-7C3A81A4C0AA","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5387890","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5387890"}}}}}