{"entities":{"Q7361892":{"pageid":31521215,"ns":120,"title":"Item:Q7361892","lastrevid":105370106,"modified":"2026-10-07T13:38:47Z","type":"item","id":"Q7361892","labels":{"en":{"language":"en","value":"Isabelle's Metalogic: Formalization and Proof Checker"}},"descriptions":{"en":{"language":"en","value":"AFP entry Metalogic_ProofChecker"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"76ed026fe057adfcc151719070396c865ed06b96","datavalue":{"value":"https://isa-afp.org/entries/Metalogic_ProofChecker.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361892$D53DCD2E-FFA5-4127-8800-C6C34AF72D0D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"661f4d8ef06d99d35e1e7e7ecc507a8b7968b768","datavalue":{"value":{"time":"+2021-04-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":"Q7361892$1E1D7654-BC94-458F-8B1C-7361E051B2B2","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"78083bbf5b06a4f292e9e00ee445948e4fa51db5","datavalue":{"value":"Tobias Nipkow","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361892$CD488EE0-4321-4234-B4FD-58EA3C71BD15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"843419218522107831692b4eb28fe996719e31f4","datavalue":{"value":"Simon Ro\u00dfkopf","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361892$F12227E1-EC9D-4426-B9CB-A94C73FB9735","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f2ce5edb55c9eca75917f50961f1cba962be7eb0","datavalue":{"value":{"text":"Isabelle's Metalogic: Formalization and Proof Checker","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361892$7944A557-C981-40AB-B99B-5BF7E0CE2217","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"dfd692263dc12a4656faf6c84efbaeb88e857ec4","datavalue":{"value":"In this entry we formalize Isabelle's metalogic in Isabelle/HOL. Furthermore, we define a language of proof terms and an executable proof checker and prove its soundness wrt. the metalogic. The formalization is intentionally kept close to the Isabelle implementation(for example using de Brujin indices) to enable easy integration of generated code with the Isabelle system without a complicated translation layer. The formalization is described in our CADE 28 paper .","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361892$4F7AD670-39AD-4910-A00C-5D0EA12EE952","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"12e4cb046e7e6d1eac10022f3d396c57882b72a6","datavalue":{"value":{"entity-type":"item","numeric-id":2754030,"id":"Q2754030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361892$203A3F14-FFD8-49B3-820E-4D65273ED434","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc9d0044875a173a7ecf2471ca493b7ca43f1fb7","datavalue":{"value":{"entity-type":"item","numeric-id":2055847,"id":"Q2055847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361892$B58F28FF-6A64-45D2-914E-B543BD4164EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1404903fbb3450c69ae4b46e148487834232fe43","datavalue":{"value":{"entity-type":"item","numeric-id":1823013,"id":"Q1823013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361892$B19FE8C4-7B5D-4853-92EC-2C8348607A63","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361892$7BB0A440-C672-4C7E-9982-856098D35165","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"e0b5465b6a0d9e05645cdb7168eee1aaf7eb2845","datavalue":{"value":{"entity-type":"item","numeric-id":7361518,"id":"Q7361518"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361892$F4C89C45-CAAF-4980-B08A-0C4C2A0FE463","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"61ce00bd57c38f4b0878e61948aa744910b408d4","datavalue":{"value":{"entity-type":"item","numeric-id":7360807,"id":"Q7360807"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361892$1456FEC3-6CD7-4FCD-88F2-0F0281100610","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361892$0F3746EE-6A7A-4C9B-9BAC-FB3229C524A8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Isabelle's Metalogic: Formalization and Proof Checker","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Isabelle%27s_Metalogic:_Formalization_and_Proof_Checker"}}}}}