{"entities":{"Q716500":{"pageid":718349,"ns":120,"title":"Item:Q716500","lastrevid":63782283,"modified":"2026-04-11T15:30:33Z","type":"item","id":"Q716500","labels":{"en":{"language":"en","value":"CERES in higher-order logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5949323"}},"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":"Q716500$0FC6987C-5342-46D6-92D0-7324D4F63B5C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d939c7b7431e750678c8cdc5af2d1ec67952d223","datavalue":{"value":{"text":"CERES in higher-order logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q716500$709D68CE-536A-4338-B675-3EB0A0E76405","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1bfb07b8f88e423f27d33c930d3d7c52d48995ae","datavalue":{"value":"1259.03071","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q716500$034135EA-2DEF-451F-AD22-5A69A06D2EC2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ac16dcce5f3df8b1bf1087e5a90fdae80fa7a2e5","datavalue":{"value":{"entity-type":"item","numeric-id":402112,"id":"Q402112"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$BD5B7E30-01E4-4170-959E-C816CEDFE2DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"53993ae6db4350dacb1d3d4f5370b18b73e58da6","datavalue":{"value":{"entity-type":"item","numeric-id":167060,"id":"Q167060"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$51CA6490-45A4-4A65-8617-0CBD9D548459","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bcfb9bbb17b1f1dc2e6c305c640f7c0f522c3f5e","datavalue":{"value":{"entity-type":"item","numeric-id":402114,"id":"Q402114"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$4763AF66-72A6-4B35-B9D7-711528B86FC2","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$D29F4F61-4337-4BEB-B99B-40355E5B0B53","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0e0f911d6f8277fb245d8e09b637e9a88b18bd10","datavalue":{"value":{"time":"+2011-09-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q716500$A30F5F4B-6E33-48DA-A640-FC21773BAB8A","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"16f1dcaadca60503d37287aa47cf4a3783733475","datavalue":{"value":"Cut-elimination by resolution (CERES) for first-order logic [\\textit{M. Baaz} et al., Lect. Notes Comput. Sci. 3452, 481--495 (2005; Zbl 1108.03305)] transforms the set of cut-formulas in a given proof \\(\\pi\\) into a refutable formula \\(R\\). Given a resolution refutation of \\(R\\), cuts are sufficiently easily eliminated from \\(\\pi\\). The extension \\({\\mathrm {CERES}}^\\omega\\) to higher-order logic described in the present paper is much more complicated. In particular, Skolemization involved in the first-order CERES is replaced here by a complicated mechanism of labels for quantifier rules in higher-order derivation, and a resolution calculus \\(\\mathcal{R}_{\\mathrm{al}}\\) used here is different from ordinary resolution \\(\\mathcal{R}\\) for type theory [\\textit{P. B. Andrews}, Stud. Log., Lond. 17, 63--81 (2008; Zbl 1226.03011)]. Completeness of \\(\\mathcal{R}_{\\mathrm{al}}\\) is conjectured, but not proved.","type":"string"},"datatype":"string"},"type":"statement","id":"Q716500$2B725406-016B-43A6-A47D-2235101909FB","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"8f432bccb81d11b6d0c5be5373ba82abf19c1967","datavalue":{"value":{"entity-type":"item","numeric-id":454365,"id":"Q454365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$389281B4-41A0-4AE2-8948-35442231AAE0","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q716500$01DDCF3A-D90D-49C3-9C4B-1F77B5626D6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6e2ae8b1900147d15ddea62ccb5302a15ee19b5d","datavalue":{"value":"03F07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q716500$CC27747B-362A-4B2E-8265-6A6DC21E7C8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q716500$72215FC2-E966-4662-B496-F0C76C0493E5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f1cee0c3ea2019a0a3c5f6b1021eefc3c103c452","datavalue":{"value":"5949323","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q716500$3AB616BA-8CB2-45AB-B289-C6A9ED5EDDBE","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dcfc1bc00c58245854e787073d98b7cbed7ce1ba","datavalue":{"value":"cut elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q716500$B7A487A9-C5BF-437C-9E38-D279FC4DB7E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q716500$96B17F1C-588B-4793-AEF2-5E87D48C708B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q716500$3D924A03-C8AF-4EF7-9473-89E1FC79C847","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"45702294177a39ee1ff9766c01d5d14dfb7896ef","datavalue":{"value":{"entity-type":"item","numeric-id":21425,"id":"Q21425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$0AAA6920-4D1A-4C32-9C27-A34EBF954CE3","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":"Q716500$9EC5AB12-A456-482B-A853-B8BB87BE05F3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"efd5c768ce435ed5138299a8d4049d5e4e408649","datavalue":{"value":"https://doi.org/10.1016/j.apal.2011.06.005","type":"string"},"datatype":"url"},"type":"statement","id":"Q716500$687DC650-8974-461B-AA7B-9F58AC46D298","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f808671057a230f1e120a64cc8c46410dbf30c0d","datavalue":{"value":"W2156662803","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q716500$34A1B2C6-27F5-45A9-8F85-08BABB5DBC19","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"388652312846c036177579ce98da69efc177622f","datavalue":{"value":{"entity-type":"item","numeric-id":5902174,"id":"Q5902174"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$0EAE28C7-2692-4ABA-9702-CB4C7887E9CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0021eb1ef45a5b93ce1d9b7eb620338bc69ad123","datavalue":{"value":{"entity-type":"item","numeric-id":5638281,"id":"Q5638281"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$D2264FE5-0B14-4E4E-A575-45F65ED8410A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"065e928c66e8a36ba87848231c1dea17453cee46","datavalue":{"value":{"entity-type":"item","numeric-id":5505574,"id":"Q5505574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$FE7B6052-1174-471D-BA76-D0EBB9B42842","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9971824e365b87038a762d44dbf9be6146ef8271","datavalue":{"value":{"entity-type":"item","numeric-id":5705944,"id":"Q5705944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$6F531279-788C-4342-9660-91813562E2A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93bcd041174ccd48e10bcb2ce475e4ab10d2f70d","datavalue":{"value":{"entity-type":"item","numeric-id":944367,"id":"Q944367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$695B4510-10DA-4BE4-82F9-981D65E54DB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b559e594edc07777117cb084e905ea94187a1df3","datavalue":{"value":{"entity-type":"item","numeric-id":4304753,"id":"Q4304753"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$BA7917EA-40C7-4174-AF6A-AAD0810CCA46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1079b6d698a143d8d07f3dc7f4c3c2ed61bd0760","datavalue":{"value":{"entity-type":"item","numeric-id":5927981,"id":"Q5927981"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$88F5B5BA-4E74-4C64-918B-20E3C1AD74F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5a779e017812886319ba5bf32e6bfca0b06d82ca","datavalue":{"value":{"entity-type":"item","numeric-id":5705916,"id":"Q5705916"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$6786D3A5-9D72-4B17-B946-5C356EBF8AF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d49380a5a0cffda5d1e1b4a498a844a9c2c454f3","datavalue":{"value":{"entity-type":"item","numeric-id":5311767,"id":"Q5311767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$2455AB00-F034-4AA8-9BF2-F3F72558A2EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"95ad3748c26d7907a9b2a2e66ec00a80dbda987f","datavalue":{"value":{"entity-type":"item","numeric-id":1868166,"id":"Q1868166"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$B7429EEB-4383-42A2-B877-83AB6752EBC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ca7e027091589776f78a6d7ad8457e805c17b28","datavalue":{"value":{"entity-type":"item","numeric-id":5777498,"id":"Q5777498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$930297B1-7343-40B4-B208-4FA58E8E9F64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b714ee7bdb70947b555d42ec2db46670455bb12f","datavalue":{"value":{"entity-type":"item","numeric-id":1431339,"id":"Q1431339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$187E0AAA-5DCD-4093-80B3-17A3519231AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"80853db170e525c88c244265a91e8196739997ae","datavalue":{"value":{"entity-type":"item","numeric-id":4894942,"id":"Q4894942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$C8117B22-D99C-4CEB-BA42-A7F33B43B8B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e74a7a357b1b46dc042b2194329594218f6b370","datavalue":{"value":{"entity-type":"item","numeric-id":1840142,"id":"Q1840142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$EC1C2537-BFA4-4E0E-AFCC-94479CF0D917","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c0f35ae7566b8bbe9c52c7114fdab5f84a63a423","datavalue":{"value":{"entity-type":"item","numeric-id":1840143,"id":"Q1840143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$9EB711B7-B161-43B9-A7B2-F77DA53ECD7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c97a7b6faf562e1c5b09260906a1f00f35a77b0","datavalue":{"value":{"entity-type":"item","numeric-id":3773876,"id":"Q3773876"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$B546D22D-50FD-4468-A32F-6727E4F4C8E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"134de46ed0f82349cd85ce2832456c9f55775fe2","datavalue":{"value":{"entity-type":"item","numeric-id":3605531,"id":"Q3605531"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$3542299F-69C0-4DC3-95B8-46BEB00DE87A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"46faa8f9dd9d2db15375b6f86cd9184a54fb226e","datavalue":{"value":{"entity-type":"item","numeric-id":5505525,"id":"Q5505525"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$75A28610-0D1D-406E-BCF2-5D5735C47EEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1675ec5894a8c57acbe2bcc56434f5813617d031","datavalue":{"value":{"entity-type":"item","numeric-id":1102282,"id":"Q1102282"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$FC78D993-62C2-4B30-8162-317D6AEAE863","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0a2b83ba84c64080a4429b9e55dc21ab47b4bb63","datavalue":{"value":{"entity-type":"item","numeric-id":3426565,"id":"Q3426565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$400E9904-D9EE-4C99-83EA-8D5C6E495434","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b0c517542965b0d42e58d2a463db711ce67c9a6","datavalue":{"value":{"entity-type":"item","numeric-id":5828993,"id":"Q5828993"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$E8E62FC0-962F-4996-9670-43962C5F9B33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"56327724d8101cacc3d4e5b36700dc86a7feb472","datavalue":{"value":{"entity-type":"item","numeric-id":4499084,"id":"Q4499084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$5AA2ACC5-C1A0-4FF5-86C0-344689003C49","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d3f6532c921c63bbde8e618ebc9ccc6b95318694","datavalue":{"value":"10.1016/J.APAL.2011.06.005","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q716500$F0284653-F65C-4022-8C24-0549888D126C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8f489b95b7f73d2dc05afaf10bdb2ac49b401c6e","datavalue":{"value":{"entity-type":"item","numeric-id":5894700,"id":"Q5894700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6cfe75c64c5c0d589d4143651caacb91ce4f9fef","datavalue":{"value":{"amount":"+0.8609668612480164","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":"Q716500$48622B43-6ABE-4D41-9665-D749A8F536B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5dff2234d712e9ec47640c786da6a18cb4b7bcee","datavalue":{"value":{"entity-type":"item","numeric-id":5705944,"id":"Q5705944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"26b57d723d6f2e994fa23292c05fd9c7107877a1","datavalue":{"value":{"amount":"+0.8580485582351685","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":"Q716500$A17486A1-7303-4B46-983C-F50E8D29EA66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"987183b865f4f446f72937c8f91496cd57b6c811","datavalue":{"value":{"entity-type":"item","numeric-id":5756761,"id":"Q5756761"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1b75045023f48f0d8695ad7ad2cd61bb43dda4d8","datavalue":{"value":{"amount":"+0.8497750163078308","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":"Q716500$8610C892-4CAB-4222-84DC-660AE7A8EF0E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f7910f50ae5a96092eb3bdfb8702ba88ad922a5f","datavalue":{"value":{"entity-type":"item","numeric-id":2259012,"id":"Q2259012"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0dfebebcfdcc5524b00ab8cbf019ebddd67c7a6d","datavalue":{"value":{"amount":"+0.8447075486183167","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":"Q716500$DE28DDF8-941F-4592-A43C-4A69C3D22A20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a747b35f96986626e096eb10bb9a93b4c83ed6da","datavalue":{"value":{"entity-type":"item","numeric-id":5747781,"id":"Q5747781"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"82a909c628f3b7abccf2a2dfeb8f95b236be8dd3","datavalue":{"value":{"amount":"+0.8403684496879578","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":"Q716500$1C63A82E-EB1B-45B2-9D57-95412595965C","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"c39a117a349789e54237c0a3254f5a10c0a6517e","datavalue":{"value":{"entity-type":"item","numeric-id":6830565,"id":"Q6830565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q716500$7CE8020E-CB6F-4FFB-B337-52DC7AFBE4DD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"CERES in higher-order logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/CERES_in_higher-order_logic"}}}}}