{"entities":{"Q6572548":{"pageid":14183703,"ns":120,"title":"Item:Q6572548","lastrevid":42356510,"modified":"2025-06-12T17:27:35Z","type":"item","id":"Q6572548","labels":{"en":{"language":"en","value":"Verifying a sequent calculus prover for first-order logic with functions in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7881126"}},"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":"Q6572548$195424F6-A3E5-47EE-B7FF-A4169F53E1A1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e13ba9221533e413dfc511c72b899926e71ad01b","datavalue":{"value":{"text":"Verifying a sequent calculus prover for first-order logic with functions in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6572548$63BC35BD-0086-439D-BE78-2B118BDFB0B1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6b28ef1f69804175267e0c47b9aca79300dfa007","datavalue":{"value":{"entity-type":"item","numeric-id":2096469,"id":"Q2096469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6572548$D4EEDA46-D1EB-4DE1-9844-B374A4435E71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"64bef53befef37231db7bcfa82edd862395ab772","datavalue":{"value":{"entity-type":"item","numeric-id":6572547,"id":"Q6572547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6572548$380DA322-BF3A-4ED5-B9D1-EFC7B7D1D676","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7dae1a09e0b079923de71e99f58f11ff9161f5ec","datavalue":{"value":{"time":"+2024-07-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6572548$1C066749-3235-49F6-9FA8-28A889897458","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6572548$1D6B7D03-97B0-4AFF-B47B-C99A2EAD2F75","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"80ce4a3b56a9a3033fc68cf6ab34e9330d751a15","datavalue":{"value":"7881126","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6572548$152E9696-90D4-42E3-A744-354448361206","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42f0513e500ea6cb630e73925875c7d53ca8d8e1","datavalue":{"value":"Isabelle/HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q6572548$0E1C4132-88BC-439C-8874-BF27F4D1D7BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0791e5718a3ebc7d54d3973aabd3f04a763d17d8","datavalue":{"value":"SeCaV","type":"string"},"datatype":"string"},"type":"statement","id":"Q6572548$F0C64BCB-CB8B-4D72-80F2-CF2BEFD4CE90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e2e80a7123e4ea6d0418cb24d37b1837f13e3514","datavalue":{"value":"first-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q6572548$3D3DC592-24CB-4806-90E7-E310F72A36B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a39411cc62ce78ebd41da7eb9d170a39ae6dbba3","datavalue":{"value":"prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q6572548$5237B971-50DE-4942-8D24-9FA6F18A531A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fe51228e17b836f3520db7bc0de40e5086eebee3","datavalue":{"value":"soundness","type":"string"},"datatype":"string"},"type":"statement","id":"Q6572548$076BD125-BD24-4018-9F59-A4C49671F1A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f6816fdf79dd11ac09d9af4886c02baab03d2cf9","datavalue":{"value":"completeness","type":"string"},"datatype":"string"},"type":"statement","id":"Q6572548$66B6BC9D-F8CF-45C6-AB36-87F2563AB15D","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":"Q6572548$D08AD4DA-9BF2-48AA-886D-69C930685383","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6b15ee75094f768b1badda85db129a0a9f611933","datavalue":{"value":"10.4230/LIPICS.ITP.2022.13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6572548$B92DF5B5-F013-4979-B0AF-FBCD7A3EFC27","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6572548","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6572548"}}}}}