{"entities":{"Q4647580":{"pageid":6677161,"ns":120,"title":"Item:Q4647580","lastrevid":53321231,"modified":"2026-01-24T17:45:07Z","type":"item","id":"Q4647580","labels":{"en":{"language":"en","value":"An algorithm for checking incomplete proof objects in type theory with localization and unification"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7002053"}},"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":"Q4647580$CD292816-191E-4F3F-8754-DF5DB983C3F3","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ee5b63aace26b62990235757d5c48b507a0d7097","datavalue":{"value":{"text":"An algorithm for checking incomplete proof objects in type theory with localization and unification","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4647580$32FC63D7-3EFE-47AD-B725-3406D6D9C593","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8df5b3c7656e4d49cf60a772c2e7b865e41acde8","datavalue":{"value":"1407.68438","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647580$B546C549-2188-438B-B1D6-71A77694A046","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2844c65e3fefbba2e55395aeaff914bf5e81e7c2","datavalue":{"value":"10.1007/3-540-61780-9_70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647580$668FFCC7-2D2B-41FA-9094-3D8F64D74AB4","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8541a6980a07ae653eb33908f7ae5402497c4804","datavalue":{"value":{"entity-type":"item","numeric-id":4647579,"id":"Q4647579"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647580$BCF61FCA-0BEE-4A66-AE72-59BAB5B8A85A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647580$5D4CB033-46B8-4B32-8832-4CF453CDFD2C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"250f083a2ef1e7a7df79afad0acdd22e5799ecf5","datavalue":{"value":{"time":"+2019-01-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4647580$CE2DF316-099C-4DB0-9769-25752CBE0878","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647580$3086554C-27A8-43E7-8EFD-D69CA77CE6B6","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"70cb7d6b6ae3423fc4e5df661644b2950cc30fdb","datavalue":{"value":"7002053","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647580$CEC6F547-BF97-41ED-8A92-01CA01593B4C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"372cb15de3004a467e66d53d6552e691fb87a439","datavalue":{"value":"unification algorithm","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647580$A8730726-3A35-468A-BAE3-955147C22F28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0bdbbb3335efa9ecfc3156c7962d1cc2567f782b","datavalue":{"value":"typing rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647580$3731E38D-FAA2-4F0C-AFEA-15743EEBA1E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6a78675f0dcb3af511ac1d4dfa61901e828bcb8","datavalue":{"value":"proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647580$5B723CEB-3521-40C7-BE85-88C349327229","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1fb5b0e94bb996d50b80f6a3cc326da05d34b8b3","datavalue":{"value":"type check","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647580$314CE901-B0CB-4E41-B47E-D75DDA01399F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"074864bccb3aca1cee29b7d2199dc711c3007ce1","datavalue":{"value":"type conversion","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647580$3F205A11-9D41-4090-B4B3-BCE83E74600F","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"05e19126d9e9907924a4600d0a5598afdc2c5f70","datavalue":{"value":{"entity-type":"item","numeric-id":20609,"id":"Q20609"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647580$3F792120-0935-40FA-A7BC-6390CF5AF3C7","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":"Q4647580$C5AAA206-70B2-4F4E-AD9D-46D0DD2079D5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"78d317790b21bb70f7b3a330cc463498382d0a03","datavalue":{"value":"https://doi.org/10.1007/3-540-61780-9_70","type":"string"},"datatype":"url"},"type":"statement","id":"Q4647580$476AF87E-5098-49D2-A3C7-255C3E86236E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e8237266b01a416663f099391ac3d694b1959f29","datavalue":{"value":"W1534130495","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647580$9132DDE0-0961-4F5A-B9D7-4534A07D6E27","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"d63e1d2c1097bf56f38b3464089e43c611b33ec4","datavalue":{"value":{"entity-type":"item","numeric-id":4939697,"id":"Q4939697"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647580$B41231A4-FF7F-4629-B305-12D06B67CF86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"27e31b151b8d22be2aa79bf2dfac73aa834ed045","datavalue":{"value":{"entity-type":"item","numeric-id":4012882,"id":"Q4012882"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647580$1B49071C-3720-4E43-917F-5932AFD8FE99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"774c18fd2b844ce5d75610805893e277658a480f","datavalue":{"value":{"entity-type":"item","numeric-id":4276174,"id":"Q4276174"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647580$A0151965-C0D0-4C1C-B664-06B6020EC87F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b9c25358477122b4737549d52e354b2ddfa62bb","datavalue":{"value":{"entity-type":"item","numeric-id":5055716,"id":"Q5055716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647580$41C88BA9-3188-4163-8665-C1D20E761C78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1eb387d93d6d1c7b34f751c3ee7736c48adf0665","datavalue":{"value":{"entity-type":"item","numeric-id":1227601,"id":"Q1227601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647580$247E0D06-689D-45E6-BCF1-B07B3E16611C","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":"Q4647580$D32D695D-07F5-4FB7-A353-6A357358F351","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47a53c9ec1ed01dcb444298314487a4908d29766","datavalue":{"value":{"entity-type":"item","numeric-id":5286030,"id":"Q5286030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647580$D900000A-4DE1-4E44-94C7-FBDC8E68A6D8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2d57aee4dc0926b14c7cd4eb20f942c2a7b85944","datavalue":{"value":{"entity-type":"item","numeric-id":5458424,"id":"Q5458424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8e10de55b5bfc02922a38c1ac05c381118a7bee2","datavalue":{"value":{"amount":"+0.7241645455360413","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":"Q4647580$A6A0D874-245C-457C-94E0-A8019FBE0180","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ac0e6455d64c974c18e666d579868b607d74d057","datavalue":{"value":{"entity-type":"item","numeric-id":5166618,"id":"Q5166618"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0aed5bb7abb1816a2bd25f275e96b6a919e942dd","datavalue":{"value":{"amount":"+0.7227545380592346","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":"Q4647580$78D605F9-1587-4EA3-93DC-3EC4E6F1ADD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bf6171f0b09d240cdab1c5988ac08fee2e637217","datavalue":{"value":{"entity-type":"item","numeric-id":3637183,"id":"Q3637183"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8b7b82518ceae52c7def9317d3949cd9e9b2b9a2","datavalue":{"value":{"amount":"+0.7171371579170227","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":"Q4647580$2ECF8540-611B-4397-A937-118529DAC037","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ad8400280694217f7467aa7b38aa90d07462da14","datavalue":{"value":{"entity-type":"item","numeric-id":3003322,"id":"Q3003322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"34f3c4c4e2e7146bf0db6332d0dbd11d0438c2a4","datavalue":{"value":{"amount":"+0.7171369194984436","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":"Q4647580$2BE2287A-3123-4DB4-A92D-69949562EB10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b180fd7c37aca86db24433ac508ad2c0acfe7e62","datavalue":{"value":{"entity-type":"item","numeric-id":4012882,"id":"Q4012882"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"89ff6e02fd7428118860bb033638fa80459f1129","datavalue":{"value":{"amount":"+0.7121091485023499","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":"Q4647580$E8ECD612-9BA5-46B9-B5EB-51904B262536","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4647580","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4647580"}}}}}