{"entities":{"Q1687726":{"pageid":1698467,"ns":120,"title":"Item:Q1687726","lastrevid":71999700,"modified":"2026-04-14T01:59:31Z","type":"item","id":"Q1687726","labels":{"en":{"language":"en","value":"FoCaLiZe and Dedukti to the rescue for proof interoperability"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6821848"}},"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":"Q1687726$A76567AB-A912-432F-8E46-3204069A9281","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0b429cd5c482f3b14d2ac8db0c3247e9eb0cfe65","datavalue":{"value":{"text":"FoCaLiZe and Dedukti to the rescue for proof interoperability","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1687726$9F594605-35FD-4855-80BA-CCDA5184EAA2","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6ac5f67854f94198e9afc8862eb00c70f49cf80e","datavalue":{"value":"1482.68268","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687726$A7256F87-0B30-44C6-8252-777575DC69EB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"80aa51627689bf7af54c28901d81afa24cbbee8b","datavalue":{"value":"10.1007/978-3-319-66107-0_9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687726$672602FF-A2E9-4130-AE89-E6D628F770B5","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c0b00160be710a75cc1195473f68075c6fed97d9","datavalue":{"value":{"entity-type":"item","numeric-id":1687725,"id":"Q1687725"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687726$7D07D000-F71A-47AA-A6BC-9C7644A66F37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f8c40e2cd3207dd1d19085f0b79e8fee7be86ced","datavalue":{"value":{"entity-type":"item","numeric-id":1624591,"id":"Q1624591"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687726$F936110E-47AD-4801-96C5-2EC5B1AEB27A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7600255b4ee907c1b1dfbc5f62c7b1165ab1b6d0","datavalue":{"value":{"time":"+2018-01-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":"Q1687726$2B72A999-4334-45F6-9C11-B62521CE8B07","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"12a655883b8e27e2d78cd16f7a449e3981dca71b","datavalue":{"value":"https://hal.inria.fr/hal-01592243/file/article%20%281%29.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q1687726$C340FD49-4692-457A-90FD-355289A7BB2C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687726$78021D1B-3C62-4B60-809C-BE00290B5380","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687726$7C86E5B8-EDA7-4D0E-8FBA-A37D66080C42","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7519b2de3adc2455c21463aef3b0f447c40bc1b0","datavalue":{"value":"6821848","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687726$B08AF8B4-CA8E-479E-96FE-45822EE041D1","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":"Q1687726$C15F41BD-73E6-4CAA-8D88-944262BB5387","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687726$373D11C0-32BE-4CF4-94D7-2546208B89C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"53a9535c02a1c0253894e545c7b8e64e868f51a5","datavalue":{"value":{"entity-type":"item","numeric-id":25577,"id":"Q25577"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687726$19AE0D95-11B6-4600-A9B7-037090D7AEAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687726$9AFA7C2D-E8A0-473E-9DE9-1396EFA3EAE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687726$14713E64-A999-44EC-8CDF-71F83D722866","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"27b6ae20da44d6f09b655d9481cc0df08a8ffcdf","datavalue":{"value":{"entity-type":"item","numeric-id":18826,"id":"Q18826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687726$CD627AC3-CD2D-4A0F-8425-01BAFE77F847","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":"Q1687726$9911F00C-E4F3-48AE-8135-2D7E1B713069","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"7e0e9d7ee9ec8072e655b5c56ed3cd495809561a","datavalue":{"value":"W2748296057","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1687726$3EA7E906-CA2F-4826-96AD-A8C9A643A0C6","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb15445443b7a8677c7ef043ed8530f20d54b0c3","datavalue":{"value":{"entity-type":"item","numeric-id":3100209,"id":"Q3100209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687726$6B198110-CC11-448C-990E-C49CF7250365","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a28f3a468e9328628410ad976d6cae50c5590f2c","datavalue":{"value":{"entity-type":"item","numeric-id":5088085,"id":"Q5088085"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687726$7FB90F9C-4567-40A4-ABB0-40DFA8756BD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad5469f72b3d14e0a040a00af8c98b8e5cf4cb2b","datavalue":{"value":{"entity-type":"item","numeric-id":3172879,"id":"Q3172879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687726$5D4AE57A-809B-4CCE-93F7-B5F0298D01EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"264a863f41b732822853937c407d70d9da64543d","datavalue":{"value":{"entity-type":"item","numeric-id":5200022,"id":"Q5200022"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687726$CDEB72CD-3882-4647-98AC-37CDA91DEE72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"70b7e36114cb3c393734b86e4e44d6b8e5d9c2d1","datavalue":{"value":{"entity-type":"item","numeric-id":3179416,"id":"Q3179416"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687726$94D045AC-0B0A-4B4F-9D8F-4908941BCEF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"751b349337ae70400cbbb8450620e09ec3b1f7a4","datavalue":{"value":{"entity-type":"item","numeric-id":2754039,"id":"Q2754039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687726$5FF100EB-2755-4DFE-B663-F1DBBF292EFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b9d10c643a95f23a54b279e960f27e43ad8b4532","datavalue":{"value":{"entity-type":"item","numeric-id":5495929,"id":"Q5495929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687726$756030C7-5EA8-412D-A3C5-805B5267047B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e0fe2d8110bad6f2e18ddd95ee07680f26231808","datavalue":{"value":{"entity-type":"item","numeric-id":654913,"id":"Q654913"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687726$79828853-00DC-4158-AC22-6BB97BF34FB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d8e0ff8a7d0c4fc199c213531e4694eacc1d9f6","datavalue":{"value":{"entity-type":"item","numeric-id":2938044,"id":"Q2938044"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687726$B4864769-B56D-44E8-906E-9B47810B2D34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb771eb1dd5ac3a4e83b6105ce84dd2191d8e367","datavalue":{"value":{"entity-type":"item","numeric-id":5327336,"id":"Q5327336"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687726$747F2FD3-5FED-4176-A32A-BE3A87FFFDB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"14084b41dac7e71956551690bb40c48e6f7029ba","datavalue":{"value":{"entity-type":"item","numeric-id":5747657,"id":"Q5747657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687726$563CB4B2-F9A2-4B1A-8593-2183B3273F25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1e46b2220dac6fabc197fa8b2340ffd4acfb8f4f","datavalue":{"value":{"entity-type":"item","numeric-id":5387890,"id":"Q5387890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1687726$CCC0C09C-B672-4670-BF73-7DE55B862905","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"670072c83b342ab9ae505897649bbd199353a239","datavalue":{"value":{"entity-type":"item","numeric-id":5082009,"id":"Q5082009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8b09d19e7c254319caea88ba252eab5430e0ab55","datavalue":{"value":{"amount":"+0.7548516392707825","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":"Q1687726$7D23817B-164C-4B67-BF59-E64B3E8D8434","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e3c3827053eda897a004928956321cc924352f63","datavalue":{"value":{"entity-type":"item","numeric-id":5435630,"id":"Q5435630"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1adf6042cf67dbb159665174638acbd804a757b8","datavalue":{"value":{"amount":"+0.7517098188400269","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":"Q1687726$0650B344-B3AF-4EF7-BD8D-5191A6442695","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d11280eec7f580346c0151d22527bb8d91725392","datavalue":{"value":{"entity-type":"item","numeric-id":2754039,"id":"Q2754039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"16f69f3039873fbdeedaa9df990196428605be3c","datavalue":{"value":{"amount":"+0.7501058578491211","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":"Q1687726$94B3D9B2-632E-46E7-94A4-41F7CD304423","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"939cd2c4229824b8a14b7f16dc661ddbc20c89e4","datavalue":{"value":{"entity-type":"item","numeric-id":5747657,"id":"Q5747657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6d88ebf1efcca0629ee13dc935380dd4a57b1732","datavalue":{"value":{"amount":"+0.7497901320457458","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":"Q1687726$B4F54B8B-FC57-4B17-AB92-307B454F59B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d619869ad0302d9b9fe0d70f22451dd60a21bf06","datavalue":{"value":{"entity-type":"item","numeric-id":2782486,"id":"Q2782486"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b9fc4d3b16bc920aaa88221d558af141cad0d860","datavalue":{"value":{"amount":"+0.7476735711097717","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":"Q1687726$B4EF6A89-B6F2-463B-A25C-ECF1EC801709","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"FoCaLiZe and Dedukti to the rescue for proof interoperability","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/FoCaLiZe_and_Dedukti_to_the_rescue_for_proof_interoperability"}}}}}