{"entities":{"Q1868509":{"pageid":1879251,"ns":120,"title":"Item:Q1868509","lastrevid":71020197,"modified":"2026-04-13T18:57:44Z","type":"item","id":"Q1868509","labels":{"en":{"language":"en","value":"Proof reflection in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1901557"}},"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":"Q1868509$F02716FB-3973-4471-A2B7-5D79E9DFF9B8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"efb639886fad35d05d0dc8fe528e9bc8c5896908","datavalue":{"value":{"text":"Proof reflection in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1868509$837DA99D-81FE-4499-B006-D0C90CC070C1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1b61b19f4ccab8d8778701b7320bd77d36875c9c","datavalue":{"value":"1012.03018","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1868509$9CD7D92F-928A-4C60-B7CC-469AE5B7A967","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0b58a9492dd4d8ab677c0de721f8d8866ab0fe28","datavalue":{"value":"10.1023/A:1021923116629","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1868509$F1AA3544-ED4B-40F9-AB61-D9752F15B480","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3ca9aba1d27cc0a527c5e55e40b675c206cdc1e1","datavalue":{"value":{"entity-type":"item","numeric-id":549187,"id":"Q549187"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1868509$9B45ED32-E8D6-4CEF-BAD4-331DCA69AA69","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1868509$FA315DAA-DA46-4925-83D7-BAC38E4FC997","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ae7235402c0b574ed2e2213feb9e21452b645cac","datavalue":{"value":{"time":"+2003-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":"Q1868509$20D311B0-3954-4F52-8B04-5E6969DB2A28","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1868509$DF8E9A07-E44F-467D-8B84-3B0578F2CAD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1868509$AFD76233-94D3-4068-BC30-FCB435BD24D7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5343d488160b5ef7b63a7fb795d4ac527f5618b7","datavalue":{"value":"1901557","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1868509$F262986F-0B90-4955-8273-EAB3ADB254DA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q1868509$4D351FE3-FFA0-4322-BDE6-0B8E0EF30AB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a74442f68c7fe9a6d53bdebbaec635290ba68a93","datavalue":{"value":"formalization of logical systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1868509$8C136572-49FF-43C9-9C30-800AAB9660F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"50b1882775c4720c2bd9796b439d3fd05a08dcd3","datavalue":{"value":"reflection","type":"string"},"datatype":"string"},"type":"statement","id":"Q1868509$08A96FE0-3E5B-41E6-A188-F934CD3394F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7245057d33d9a959e820bafe53b372c083536e6","datavalue":{"value":"natural deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1868509$88B10E79-1D1D-44E4-819C-1DBCFFD3D6C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e2e80a7123e4ea6d0418cb24d37b1837f13e3514","datavalue":{"value":"first-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1868509$203A258F-5EA4-435C-9007-2E4FD30BEF01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ddb3b09c730392dd3ef6993ef5a5aa809f6b412","datavalue":{"value":"reduction relation on proof terms","type":"string"},"datatype":"string"},"type":"statement","id":"Q1868509$5EF6523D-591C-496F-9F26-9A826589C4F5","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":"Q1868509$64D07B2B-0D45-46A5-BD20-267F4D3A0392","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":"Q1868509$D5199BA5-9E6B-49E2-BC77-C34B1A1FD8BE","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ec1b7886967e6b043c68abb3cba95c33dcc052fd","datavalue":{"value":"https://doi.org/10.1023/a:1021923116629","type":"string"},"datatype":"url"},"type":"statement","id":"Q1868509$03BCFB31-0201-443D-9DA5-AE328E894ADC","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"caa94107b86aad17be165bb7d881728a69555ac5","datavalue":{"value":"W1611906969","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1868509$AFD2D62B-5CFB-4805-9404-FC7D584EF807","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1813dee6ade6ce3af2af73d2234b94398df48393","datavalue":{"value":{"entity-type":"item","numeric-id":5958299,"id":"Q5958299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"410da64645666f7a4968a8cb08f8e8d4cb559808","datavalue":{"value":{"amount":"+0.90664005","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1868509$72895EA4-AEAF-4314-AF92-A245515EF0F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0cf20a72c87c85cf6f836cdd293a539c83e95161","datavalue":{"value":{"entity-type":"item","numeric-id":1332853,"id":"Q1332853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"29d0a46c72d7fab1ce999ab0155f5b5f5d2beca2","datavalue":{"value":{"amount":"+0.9046178","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1868509$2CF7BA68-E4C1-4072-96A4-5D37BA4EF91B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"87b6ac01518a02a5afd884695660984f387da000","datavalue":{"value":{"entity-type":"item","numeric-id":2766536,"id":"Q2766536"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"503f9afb53a624218d4c3e5f4ffc5cf69668b62f","datavalue":{"value":{"amount":"+0.88396066","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1868509$6686ED68-0E3E-466C-AFCC-4774524A099B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"769937c0838347b6d65d7cf565f4f4b02f76aadd","datavalue":{"value":{"entity-type":"item","numeric-id":3138833,"id":"Q3138833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"846e0e665f5ead73805e479e90f7fc3d9f404163","datavalue":{"value":{"amount":"+0.8796701","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1868509$F07C62C2-4AF5-40C0-8401-05417AB49C37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3749e69383bed0e4adb0bf8499ddab1bc0cbd6c7","datavalue":{"value":{"entity-type":"item","numeric-id":3075246,"id":"Q3075246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"da5f0743da109dd85fe70645a61624f65a69e441","datavalue":{"value":{"amount":"+0.87730914","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1868509$0CCE2C58-63D7-4507-974E-D5BCF3F77D9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e26c3ee28b2edb7374449f2f1032135d4fba7d2a","datavalue":{"value":{"entity-type":"item","numeric-id":2798255,"id":"Q2798255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"264e084d82f16f37291d37f0f34f705d8da629e2","datavalue":{"value":{"amount":"+0.8737085","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1868509$BBEFD360-976B-40D7-9757-3085CB2C67E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5858a5c465ae509dc6d99ac5a58665a02a243cb8","datavalue":{"value":{"entity-type":"item","numeric-id":5048991,"id":"Q5048991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7025556393f823a081bd59acb0a82e48a257fcdc","datavalue":{"value":{"amount":"+0.87342477","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1868509$BA1763A2-10A0-4DD9-8A1F-F28190C39887","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3f6f497407874e3ab164c554c350f73fc98fdbd0","datavalue":{"value":{"entity-type":"item","numeric-id":4989018,"id":"Q4989018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1bfd8073b6929dc2a6b5d4f2ba4878ed0d23ae53","datavalue":{"value":{"amount":"+0.8692324","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1868509$2F485E36-D2A1-475F-AABE-3BEA3E19F7F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"329f1adbc39f65eb0ddb334a90cf786ac108a9f3","datavalue":{"value":{"entity-type":"item","numeric-id":1687728,"id":"Q1687728"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"510f52193f56200544b1f9159354736e1b904e89","datavalue":{"value":{"amount":"+0.86834025","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1868509$3590F6FD-08C9-4E62-83E0-665F8A8024A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"46bffc769a858c4d2ae6ca9be48397887233ffad","datavalue":{"value":{"entity-type":"item","numeric-id":5875438,"id":"Q5875438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ea66fbd1280b69ee4d7ea8cbfe09b1fbd00177bf","datavalue":{"value":{"amount":"+0.8679879","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1868509$35D30287-E3D9-4F38-9049-636CF9A4C5C6","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Proof reflection in Coq","badges":[]}}}}}