{"entities":{"Q5875438":{"pageid":7904989,"ns":120,"title":"Item:Q5875438","lastrevid":93267572,"modified":"2026-06-05T04:06:30Z","type":"item","id":"Q5875438","labels":{"en":{"language":"en","value":"Ornaments for Proof Reuse in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7649975"}},"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":"Q5875438$3BA77E4D-9ED0-428A-AFFA-1BBD50DEDAB4","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e7c05f0104b3f3b9ccdad656b95b8313ca4a020c","datavalue":{"value":{"entity-type":"item","numeric-id":5875436,"id":"Q5875436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$F3A7919B-CB91-42E0-8260-B0310499312C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b10a0fa1eeefe95447df0ddf0a39b111c676a239","datavalue":{"value":{"entity-type":"item","numeric-id":5875437,"id":"Q5875437"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$9F2AF4D6-0A69-4A9D-AC6B-A8285CAEBE0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7b16f1bc6f41c7a774a060975e1d55a96996f239","datavalue":{"value":{"entity-type":"item","numeric-id":1297480,"id":"Q1297480"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$C08A4A5A-0639-4998-8524-DC3F9E9AA05E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5d68fb6b2ee58deb1f5b14ec34618df78bd8bd62","datavalue":{"value":{"entity-type":"item","numeric-id":2817721,"id":"Q2817721"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$74638943-11DE-4A57-958E-034A946A7D61","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6695abe38664d65c38747de7b5fe54d9caa92dea","datavalue":{"value":{"time":"+2023-02-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5875438$FCB14011-9FE3-4044-9875-5591F1686655","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875438$7C8D7BB8-873D-4D58-95A4-B05BCE7996A3","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3ba5e0a04d32071d1604974dc4daba863ff4d996","datavalue":{"value":"7649975","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875438$D5070B28-91A2-4D65-A7EE-ACD998521DD8","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"70f6590d323ffcddfecf63daf32f510770f7a2e6","datavalue":{"value":"ornaments","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875438$2E5F68C6-F5CD-4850-8F08-F617A293A5F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"debc1a7decd93e19a2dd0ca968e424e5ba0618ef","datavalue":{"value":"proof reuse","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875438$87DA306A-4001-4FCE-A5D7-13183047B098","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d62798ced101241ac0d5e46110e32d69e73a0c1a","datavalue":{"value":"proof automation","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875438$5A81DAD3-A9C7-45AC-835F-B3B94743AD51","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1f427ab6dbbd025b0c0b66dd047be36c332e9e80","datavalue":{"value":{"entity-type":"item","numeric-id":32822,"id":"Q32822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$6534B5C6-78E8-40FD-B5AA-8AD4F8A6D673","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e9fd7dbff509abaee9c64d21afb19f85055bad01","datavalue":{"value":{"entity-type":"item","numeric-id":32823,"id":"Q32823"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$D1C1A7C0-32FF-4B0C-8911-6728234A6A92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1b943e49a9f344e0780b3d3e4fc5e87f0fb22800","datavalue":{"value":{"entity-type":"item","numeric-id":31804,"id":"Q31804"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$83DA2DC6-7E0B-44C2-A515-33F7B203353A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b29eb58b948f9f996cbb5eae736ddbdaf0434b06","datavalue":{"value":{"entity-type":"item","numeric-id":34514,"id":"Q34514"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$B0ECFEDE-EA66-4D79-BD75-09A67ACF03C8","rank":"normal"},{"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":"Q5875438$23027D13-3557-41A1-A704-CA02B36DAD99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8bf42d0fd66acf369e3d5d44d7ebef6adc7ae452","datavalue":{"value":{"entity-type":"item","numeric-id":56651,"id":"Q56651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$8CD97821-8109-408B-9FD6-C16CBC1BFB14","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":"Q5875438$1E7A6A39-59D4-43D0-B00E-634F2EF92383","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"19bfc71a57d8b53745c227c7b28296ee04920269","datavalue":{"value":"https://dblp.uni-trier.de/db/conf/itp/itp2019.html#RingerYLG19","type":"string"},"datatype":"url"},"type":"statement","id":"Q5875438$946703A6-E751-401E-BB09-411EB5CCD8DE","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b97d51ea23689af813f5ae5aacaf274f1295ffe8","datavalue":{"value":"W2978136495","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875438$C71730A6-2351-49D8-90D0-A0F2732ECFCA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f9c1ece2a6b2542d2fd20e770dad31023fc11e59","datavalue":{"value":{"text":"Ornaments for Proof Reuse in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5875438$8C354889-E870-4310-A576-55B78184C0AC","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd91fe16bf6787b38a2cfa6e724a7fcabfd5b080","datavalue":{"value":{"entity-type":"item","numeric-id":2769425,"id":"Q2769425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$3D957365-AF8E-4D49-B7C3-4DD2EBAF0493","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"95fab8824d82d4ca6fefb7d000ea15dc3e260bd1","datavalue":{"value":{"entity-type":"item","numeric-id":2844694,"id":"Q2844694"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$8B305EA2-236E-47D3-A031-DCA41FA7B81E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4fd098ea4c8653eaec826e6d53d5157343c914f","datavalue":{"value":{"entity-type":"item","numeric-id":4580226,"id":"Q4580226"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$CB51792D-4ECE-4C23-B397-586B9AF41408","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ceea143bd1bfcc6da3c06302f6586883957ef3a6","datavalue":{"value":{"entity-type":"item","numeric-id":5372005,"id":"Q5372005"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$F8E4916B-C2C5-410E-BA3C-BDE708AC1301","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8aea8e681efb8035e811bf81566cee467f9c1736","datavalue":{"value":{"entity-type":"item","numeric-id":5271091,"id":"Q5271091"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$A440C6F2-5F9F-436E-BC43-F41D6557832B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6d31dbdebeaa77beca51692d4d8f013221761ef7","datavalue":{"value":{"entity-type":"item","numeric-id":2875233,"id":"Q2875233"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$85A0F788-CB2E-418B-8BFF-3C0F365F5D26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8bf3dba72f9cb3aa976e9fb209aa77966813aebd","datavalue":{"value":{"entity-type":"item","numeric-id":2931797,"id":"Q2931797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$AD875A02-8BE7-4DEE-9310-4C51E5A95BFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"18fa226924cc974ee1c50efee3ff193344791f61","datavalue":{"value":{"entity-type":"item","numeric-id":5210800,"id":"Q5210800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$4C349159-3B5D-450F-A299-5FB4669548D4","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":"Q5875438$10EF3919-71A6-4720-84F6-1E17753484CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"50bfa2e117edb9cc1db8207f4a56b574498f0c14","datavalue":{"value":{"entity-type":"item","numeric-id":5464644,"id":"Q5464644"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$AC9C5345-71CF-4C94-B19A-9AD891F26B07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"74ff5103126771aaf1c73985cf867755814084aa","datavalue":{"value":{"entity-type":"item","numeric-id":5372000,"id":"Q5372000"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$D0A10F22-2276-434C-A2BB-9F861B72DDD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d60ce31f335bad429a6e1e462b560a699f61e298","datavalue":{"value":{"entity-type":"item","numeric-id":3559761,"id":"Q3559761"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$0EACC8B1-64E8-42FF-A25C-EDE6BE75B3D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5dd7e9167e724225c18f70e1bf89bb810151a73f","datavalue":{"value":{"entity-type":"item","numeric-id":4736398,"id":"Q4736398"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$6C2F5364-E71C-4C65-80FE-DF873ABB7765","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"abd41ddfdf765b977d07c744981cc2ca02fbef55","datavalue":{"value":{"entity-type":"item","numeric-id":2985783,"id":"Q2985783"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$B55DBF77-777F-4DB5-BE43-5F51FBF28DD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5f17fc4ebb3d30ace7bc9fc38c3b78079904f92","datavalue":{"value":{"entity-type":"item","numeric-id":4736400,"id":"Q4736400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$F6DC6C86-7313-4B1E-A6EB-6D16F5C1FCC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a2ea19df45b380e856eb67512942460b3fe49455","datavalue":{"value":{"entity-type":"item","numeric-id":5747666,"id":"Q5747666"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$26E0485B-DBC1-4701-8C7A-FFDA42615EDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d70582cce52cae0af3a214a6e235592df5ddb652","datavalue":{"value":{"entity-type":"item","numeric-id":2787453,"id":"Q2787453"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$0B54E284-B2F4-4880-96B9-1B33519C7D91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"890522dc4e3ecb3007fccfde8c53acf4163b6c1a","datavalue":{"value":{"entity-type":"item","numeric-id":5420262,"id":"Q5420262"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875438$709644C0-D514-4AF5-83BE-1348E76E4B6F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"32558cacfbfe62b3ba5cb754a2ca4c4bef9c22fe","datavalue":{"value":"10.4230/LIPICS.ITP.2019.26","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875438$A8AEF14A-45B7-4C9D-8642-33485857C400","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Ornaments for Proof Reuse in Coq","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Ornaments_for_Proof_Reuse_in_Coq"}}}}}