{"entities":{"Q5756497":{"pageid":7786048,"ns":120,"title":"Item:Q5756497","lastrevid":40922853,"modified":"2025-04-14T04:27:57Z","type":"item","id":"Q5756497","labels":{"en":{"language":"en","value":"Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5187155"}},"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":"Q5756497$7A6182EC-8BD2-4212-94CE-20EC4FA62230","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f00709991a5bb14c6ea1d40e3725c3957356bd6b","datavalue":{"value":{"text":"Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5756497$5CFD15AA-85BB-4A3C-9934-380C17FDA9BC","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a311bd1295771b43faac2374fdc393a2d007ec99","datavalue":{"value":"1187.68141","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5756497$D1757521-CDE0-4489-8A44-DE68FBF57A08","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"77999b56e81da3f25fb17c949bc5f88282ba6307","datavalue":{"value":"10.1007/978-3-540-71316-6_15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5756497$398E98E6-00FE-44EC-A785-9E06791C6BBC","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"2ae562a9b4ab01b03508d01f680612b0713f587c","datavalue":{"value":{"entity-type":"item","numeric-id":249846,"id":"Q249846"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5756497$1CB9568D-BCE5-4511-9F08-AA1635C41B17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"57155b56d8fbcd7c5881cc6580886a49385bb630","datavalue":{"value":{"entity-type":"item","numeric-id":287360,"id":"Q287360"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5756497$4FF74BB7-692F-4B9B-8E98-30067CB386AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1d512f15aa7dca5445b4f70135bf8aa67126d08e","datavalue":{"value":{"entity-type":"item","numeric-id":1029814,"id":"Q1029814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5756497$8261D709-6429-41E8-AA2F-B1EACF7C50CB","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7efb66db9d8cc237b51d0f645d1a54c929d4c460","datavalue":{"value":{"entity-type":"item","numeric-id":2789030,"id":"Q2789030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5756497$BDD33684-B4FC-4E75-9956-A1D0E10C22DF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"425e48b9986b227b93d91ab0854d5e88273c1020","datavalue":{"value":{"time":"+2007-09-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5756497$B73DBD8D-D258-442A-BFEF-F046DA1CC460","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3affb2aa66be15f2a63c60d2aaa92bd143e6d46","datavalue":{"value":"68N20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5756497$4875346C-F928-41E2-927E-35172BFFEE43","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"058c2ec3d9476179e46037697ba6075e7bf93a8e","datavalue":{"value":"5187155","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5756497$AAB6832E-5BB7-4D64-9AB1-07BB8AA20472","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":"Q5756497$5319DB7C-5058-4BD1-8FC1-A0D5F6169828","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"05d337b084bb4ef0cdee47f4be4854a8c9112804","datavalue":{"value":"https://doi.org/10.1007/978-3-540-71316-6_15","type":"string"},"datatype":"url"},"type":"statement","id":"Q5756497$46C1D12B-B2A9-4B3E-A219-6D06BBB9F91F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d9e05064610498181eedb681a0a8ca4fad57c795","datavalue":{"value":"W1536568106","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5756497$7870E2F6-E677-4E5C-8950-8A44781A3659","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"116ae40af25df1caab31ce7865056cc8623f9e19","datavalue":{"value":{"entity-type":"item","numeric-id":3789101,"id":"Q3789101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2831a829166322f36a320d6e14a8204db3dc9401","datavalue":{"value":{"amount":"+0.9075017","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":"Q5756497$42766327-468E-4EB6-B386-569A8BA010F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3b59b8ff94a887eeacfa89279cb7525faf9fc91b","datavalue":{"value":{"entity-type":"item","numeric-id":4944869,"id":"Q4944869"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d65ddfdfc0b7fffeccc128fc55e4d863242b429c","datavalue":{"value":{"amount":"+0.90608525","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":"Q5756497$593695B3-3A4F-4943-8D60-12677319A854","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9d5323e680a7c6c14f0810023060c0fa576c7a95","datavalue":{"value":{"entity-type":"item","numeric-id":4911140,"id":"Q4911140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4d766ace602ecde29216c8198eebfff37ea2710e","datavalue":{"value":{"amount":"+0.9033978","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":"Q5756497$DBC990F8-2647-4A5B-BA1A-D43F7E88486D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8139328ea45d0f5f4bbb53ec8e07615b518a5b98","datavalue":{"value":{"entity-type":"item","numeric-id":3578399,"id":"Q3578399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"13b1687f22c821e64f039ae35362607069e7f8a3","datavalue":{"value":{"amount":"+0.90146273","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":"Q5756497$302212A9-9FD9-48BC-8BFC-C37DA8760A7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7ba65f6a58ed08b60fa73248e76ff032f9c8be87","datavalue":{"value":{"entity-type":"item","numeric-id":2722041,"id":"Q2722041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"caa8716341e57c7c06b5d5814a3ec8c9fc22c57f","datavalue":{"value":{"amount":"+0.8980841","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":"Q5756497$28F9FE5A-63FC-4F45-BA8D-40C40D5190DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"78478b8769b76feb7ae990961e17dc2fa8626324","datavalue":{"value":{"entity-type":"item","numeric-id":3510441,"id":"Q3510441"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"59fe80ca9f2094b298b6a4fe8d28bbc7cc52b037","datavalue":{"value":{"amount":"+0.8974178","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":"Q5756497$5AE1C99D-1EC4-4891-9217-28325DBFBC4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"779aa4f2e95d3d3e046cbe92464281ba0bd157d8","datavalue":{"value":{"entity-type":"item","numeric-id":2767046,"id":"Q2767046"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0a4a90f2115dc4dd5bafa98fd1a45c28d011860b","datavalue":{"value":{"amount":"+0.89543444","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":"Q5756497$54F2D91C-9DBD-4BB8-B70F-FE9C399EA7B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"534ab4cc528829f573af9e6705220481f24ef1c0","datavalue":{"value":{"entity-type":"item","numeric-id":5168887,"id":"Q5168887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6da22f5c81f248a64f9ef89f6f3b61fe0299192b","datavalue":{"value":{"amount":"+0.89384663","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":"Q5756497$7F89DDB4-3530-4EC7-B63C-094558150591","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"56258b2756d046fcc6a752e9d916b34329ac2d5c","datavalue":{"value":{"entity-type":"item","numeric-id":853741,"id":"Q853741"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9c2ac694d472af442823f54b8934ba86d2e60869","datavalue":{"value":{"amount":"+0.88933975","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":"Q5756497$F1EAF12D-451A-41DD-B4EF-A1B0A2A5D938","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ee9691043fc2fa83f9bcad490e83cd2b178847bf","datavalue":{"value":{"entity-type":"item","numeric-id":1987736,"id":"Q1987736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5af974effb513556631890fc0312b80ab36c7a16","datavalue":{"value":{"amount":"+0.8860488","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":"Q5756497$FEA7E510-340D-4156-843B-8ADBCD9A8639","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5756497","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5756497"}}}}}