{"entities":{"Q5028472":{"pageid":7058049,"ns":120,"title":"Item:Q5028472","lastrevid":58401345,"modified":"2026-04-05T01:34:41Z","type":"item","id":"Q5028472","labels":{"en":{"language":"en","value":"An extensible equality checking algorithm for dependent type theories"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7471706"}},"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":"Q5028472$2110DF8B-2030-4A92-B5E9-91304E1EEC65","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f1ac28f142a3cce7e0b0063bd84435e8a2ed302e","datavalue":{"value":"1504.68276","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5028472$5B4B54A4-E7A7-4B39-8FB9-5CD1FB0E80B3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0f2df3919dd6f0285578bf9d7f4189831f0dfe16","datavalue":{"value":{"entity-type":"item","numeric-id":390413,"id":"Q390413"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5028472$B84C950A-B900-4094-80DA-A4A16036C3D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7c1ddc7c87ccd4acfce96a5417e0b991236936b1","datavalue":{"value":{"entity-type":"item","numeric-id":5028471,"id":"Q5028471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5028472$82EBA813-57C5-4C23-90B7-305E74A438C6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"016f5c9439ba374a39d268cbe8a17a8d3cb3913d","datavalue":{"value":{"time":"+2022-02-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5028472$69495A08-4DD5-42B1-844C-CFA3BFE40EA0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"cb4e6ecb5d0cbcfba8bedbe9f252edcb9120c07e","datavalue":{"value":"https://arxiv.org/abs/2103.07397","type":"string"},"datatype":"url"},"type":"statement","id":"Q5028472$F7ADBEE9-F1DB-46CE-A7D2-245F4871A095","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P205","hash":"8e3a832639e8d47b4eb1c78c292983eb4439153a","datavalue":{"value":"https://lmcs.episciences.org/8980","type":"string"},"datatype":"url"},"type":"statement","id":"Q5028472$59C42E09-FA7F-4F89-BEF8-9103784AEDCF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5028472$35AA776B-1AB3-484A-BC7D-866C5EEF77EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d9230c8da6e5632ad621620269b7ca185454f9df","datavalue":{"value":"03B38","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5028472$8BE4EEE2-2265-456A-8C99-85786482438C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9a5bf3ad59417e386b1dbe638fd35fa83765f5de","datavalue":{"value":"7471706","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5028472$19076267-132C-4006-89A3-BF84413E73DC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5028472$CE6BEC89-9D9E-4002-8C9C-434BC42F64F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"65a5117cb6ddb103d035928761912e8be0006673","datavalue":{"value":"equality checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q5028472$345A2EAC-0FC1-4330-A8CC-13F954341DA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6a78675f0dcb3af511ac1d4dfa61901e828bcb8","datavalue":{"value":"proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q5028472$9F974B19-24F9-4026-B9D5-2812147360F8","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"39d1d25ae8c00cfad058b188db36fd61dac09925","datavalue":{"value":{"entity-type":"item","numeric-id":27041,"id":"Q27041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5028472$D10B0121-390C-4606-86E5-F39AC9C1C518","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":"Q5028472$AC98E5F4-9A97-4B75-9C08-5F390673EB7F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"833079337a3c2f303ddbc3fe894c26799c99160e","datavalue":{"value":{"entity-type":"item","numeric-id":2881097,"id":"Q2881097"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5028472$D8BBB08E-353C-44F5-8E7F-91EE89870F0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"73e9b88cd02705fdfc205f06a1c9373e773841a2","datavalue":{"value":{"entity-type":"item","numeric-id":5041060,"id":"Q5041060"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5028472$DA1A00CF-D73F-4F36-9031-D48EABB41EEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8fac7c6d05f114a4ae2738237ef25b8c9ead77ff","datavalue":{"value":{"entity-type":"item","numeric-id":1945914,"id":"Q1945914"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5028472$3FD7EFE2-3C08-4688-A3EE-A47F362E324D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c55279b562077235a83c8f027abb8a1db79401d8","datavalue":{"value":{"entity-type":"item","numeric-id":3194730,"id":"Q3194730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5028472$76B8C842-DF4D-4E95-81A2-9578D5720C38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8242928870aab67343ad0152eb7ca8357168f7f3","datavalue":{"value":{"entity-type":"item","numeric-id":3454108,"id":"Q3454108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5028472$CC882B28-8729-4322-B518-C4E6E56FA846","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"347ff5e243a44fe280b61636b43f4d0e72b66679","datavalue":{"value":{"entity-type":"item","numeric-id":4281480,"id":"Q4281480"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5028472$BA3FD04A-436F-428B-89C7-77214472CA61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5d284d3472d35d2cc3b63390bb184a9355795123","datavalue":{"value":{"entity-type":"item","numeric-id":4617969,"id":"Q4617969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5028472$42099ED9-0DC0-45D6-860F-A317638AFB51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"69fe664aa22c6ba1ea6d9ba12c2b4c3da0298ee2","datavalue":{"value":{"entity-type":"item","numeric-id":5277760,"id":"Q5277760"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5028472$5CA8E13A-D660-4E75-9F8B-A64BA90F3B81","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ca8be57c31586c697de9de588782ed0ea81a6eb3","datavalue":{"value":{"entity-type":"item","numeric-id":5041060,"id":"Q5041060"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2c9eb9cb160df48a9509167bc1bb30ebdcadbd34","datavalue":{"value":{"amount":"+0.9050768613815308","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":"Q5028472$985FFBC8-2783-443A-A37A-96D3B2FEC2B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5688ed66a44257c423ffa0f6cb24d2c0a8e4433a","datavalue":{"value":{"entity-type":"item","numeric-id":4645754,"id":"Q4645754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e4c8ad374f91c8a74568359c79d769acbf92aeb0","datavalue":{"value":{"amount":"+0.7478963732719421","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":"Q5028472$59C51125-4111-47FA-B6D6-76FF3C7278A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e703c12462fa3c0b4409c4b169c76db5afa7ad9a","datavalue":{"value":{"entity-type":"item","numeric-id":4500363,"id":"Q4500363"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c3a629a62acf09a5caf59e750263918324fbe914","datavalue":{"value":{"amount":"+0.7468633651733398","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":"Q5028472$7E0FCDA8-B4E6-414C-A56D-369CE6B1B719","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e62e08aae69bf14a5dee004999b6c7f37287ffbc","datavalue":{"value":{"entity-type":"item","numeric-id":3521979,"id":"Q3521979"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fe3039a5c039069d8d70e7b3030ceaa40ee82c9c","datavalue":{"value":{"amount":"+0.7415563464164734","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":"Q5028472$2E06E556-6C22-4F58-9750-C1EF4D1E20D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"270de6527ae96c33d421a94a582ab741c9b0b3f7","datavalue":{"value":{"entity-type":"item","numeric-id":5705901,"id":"Q5705901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"31bf1549d4e5ba1ebc72981d80bac085470f0cf7","datavalue":{"value":{"amount":"+0.7402994632720947","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":"Q5028472$00938079-137A-4F68-8AB3-5757D27E4204","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5028472","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5028472"}}}}}