{"entities":{"Q2142084":{"pageid":2152827,"ns":120,"title":"Item:Q2142084","lastrevid":43592623,"modified":"2025-10-28T01:34:31Z","type":"item","id":"Q2142084","labels":{"en":{"language":"en","value":"Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7532523"}},"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":"Q2142084$0522E63A-E5A9-458F-BAE7-FB115EB69325","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"60dab125a5892895b037727a2e9f327e8db4b0fe","datavalue":{"value":{"text":"Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2142084$430521CE-3C5E-4304-89DA-D53028EC1EF7","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1be5c8cf0c46bbdb8dd549f96be3c63e7e1856b0","datavalue":{"value":"10.1007/978-3-030-86059-2_18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2142084$06860C74-9440-4C17-92FA-06D12CCD6EB6","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9764b5e3183836adae29ba3fef393bcd0832967e","datavalue":{"value":{"entity-type":"item","numeric-id":229747,"id":"Q229747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142084$53CC83F7-A8C9-47BE-9061-4D2D38BABC8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4cd26fdbdfe1d2fb01e4aa125652a423d7111de5","datavalue":{"value":{"entity-type":"item","numeric-id":1709694,"id":"Q1709694"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142084$2C4DC85A-A570-4F18-B5F9-D69F7E45C06D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e9416262b1a929f0f1cc54516469cf47a3a7887c","datavalue":{"value":{"entity-type":"item","numeric-id":2142083,"id":"Q2142083"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142084$AA123D28-2956-4129-B4AE-8DA6B4919472","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"12ef1e2e38c147b52c379a6993b1283d5267f8ef","datavalue":{"value":{"time":"+2022-05-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2142084$A42A5A98-C325-4D8D-98CA-7283AAD68350","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2142084$F430DAE4-00A6-41B8-B4E0-E9AA7DE5C989","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0297de7bc35d07aff9bbb598c1d676a75ad3c006","datavalue":{"value":"7532523","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2142084$6D2B7E20-7A45-4273-B969-A2B202ECB7C2","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f8d8b2ba2dab9cd7a0abecc72ba85c506d4e76ba","datavalue":{"value":"provability logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2142084$CA971F10-1FC6-460F-9FBC-8387623AF7C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b117cf251cec88c66a52b2392d0867e5e86e7ff8","datavalue":{"value":"cut admissibility","type":"string"},"datatype":"string"},"type":"statement","id":"Q2142084$CA04531B-9FB7-47F8-BD60-58DA7E7BC5E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2142084$9538A455-A46D-4B42-9BC2-6B573D930476","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"83d5dcaa7aef3dc9ddc3eab92a7db35d53442c07","datavalue":{"value":"proof theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2142084$482417C7-5D5E-4B96-8E01-279BAFFC377D","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142084$6445C1C2-5B7B-4CF4-90F2-AC501F89AE46","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":"Q2142084$EB8A1D97-AB06-4092-9D22-B52D5A2C50EE","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8d042ffee05bfe3487f98967385f93d58d5b294c","datavalue":{"value":"https://doi.org/10.1007/978-3-030-86059-2_18","type":"string"},"datatype":"url"},"type":"statement","id":"Q2142084$CC42D7DF-2803-4B5C-A388-38A699D5A12D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"6f8c9758de3a71af7b4e85297cadc83722b9d726","datavalue":{"value":"W3197466636","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2142084$C0962819-85EE-4BFE-BBF0-CBC2093DE104","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"9210648c2da7d5773e848b729398c42f3567a36c","datavalue":{"value":{"entity-type":"item","numeric-id":4196401,"id":"Q4196401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142084$78D72736-A8B5-4BDE-8695-D82D203EDF40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fcfc8403876b09cb2cc770b8d6fb399a97b6112d","datavalue":{"value":{"entity-type":"item","numeric-id":798649,"id":"Q798649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142084$F8844B02-88F5-4F12-9AB3-FE66EE29D606","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fe3a9192ba70313d578f72b18f3e6569f6312686","datavalue":{"value":{"entity-type":"item","numeric-id":288243,"id":"Q288243"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142084$749CF0C0-FE62-4989-85EB-7B4C4683B8B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"66f272d7287f994bc6a285690f7059c71fa20c01","datavalue":{"value":{"entity-type":"item","numeric-id":4933310,"id":"Q4933310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142084$ED2B6F0E-E8F3-4587-8A20-A080A8EB3EE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ff1c9576a9af1e44009a9ef9a0f7f22e091829d5","datavalue":{"value":{"entity-type":"item","numeric-id":5610986,"id":"Q5610986"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142084$1AB59CD4-0432-44EF-B0C9-5C45CA8153BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aba4829fd07b9b49631e42171c8fc19ce2487bfe","datavalue":{"value":{"entity-type":"item","numeric-id":2890695,"id":"Q2890695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142084$F7F3EDEE-D615-468E-B612-B17123262D04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65ab817940069820fabea9c24df7b4537fbed9d5","datavalue":{"value":{"entity-type":"item","numeric-id":2016062,"id":"Q2016062"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142084$F4EAB9B1-31F8-400C-A88D-F17937BC1DC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1fe209441d22f37cd11506b828135c8648f716b4","datavalue":{"value":{"entity-type":"item","numeric-id":4565826,"id":"Q4565826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142084$15D58797-09A9-4890-86D3-9AF60A463A21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8546dfa3ee45536454a034a5905b0e5f07e2b82","datavalue":{"value":{"entity-type":"item","numeric-id":812101,"id":"Q812101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142084$4E509035-0E5A-4101-A623-1C6F4ADD3D1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a05b88e8939da5afe0e37d672faef2e7bfef9975","datavalue":{"value":{"entity-type":"item","numeric-id":2254557,"id":"Q2254557"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142084$2385F691-92E2-4FF3-9A8E-483ABFF0B693","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b767d85950bf99e8910526fcfcbcb504d6a930ba","datavalue":{"value":{"entity-type":"item","numeric-id":1056745,"id":"Q1056745"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142084$F36A6E48-5B07-476A-B369-EE79EB0C5925","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"803595e33b228fa6775e4c45b15092a5bcd4f221","datavalue":{"value":{"entity-type":"item","numeric-id":2303617,"id":"Q2303617"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142084$1AE2A1B8-C70A-4CB0-B5E6-399E4963EF8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65af634f8ea04e9717486b98f2f6b61acf5b154f","datavalue":{"value":{"entity-type":"item","numeric-id":1235695,"id":"Q1235695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142084$C3DF60A0-5FFB-41A5-B747-CF35E6D71717","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9046092912369ae53c021eb53125c7bea4658d3d","datavalue":{"value":{"entity-type":"item","numeric-id":790809,"id":"Q790809"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2142084$A1304397-B165-4378-9680-EB6E6BC2F5D8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2142084","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2142084"}}}}}