{"entities":{"Q4650285":{"pageid":6679866,"ns":120,"title":"Item:Q4650285","lastrevid":48410890,"modified":"2026-01-04T15:42:00Z","type":"item","id":"Q4650285","labels":{"en":{"language":"en","value":"Proof normalization modulo"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2133232"}},"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":"Q4650285$C3998081-DC58-4E83-B3C1-68B90BEDD5B2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d97f1d99e014d8003cfd9358f175770d37a63cb8","datavalue":{"value":{"text":"Proof normalization modulo","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4650285$91ED3EDD-FEA8-479B-9C12-33D3A6F02F81","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e21edb7c94c6596941078bb0e99c4dfd832eb01e","datavalue":{"value":"1059.03062","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4650285$C8D00283-B045-4A45-82CA-AB2B1E09F093","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f681530f1e601559ae451198ac16d4e80569d32e","datavalue":{"value":{"entity-type":"item","numeric-id":436401,"id":"Q436401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4650285$26B10B89-66CA-4179-85D0-BA1F7AE71009","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f69fec18e304e301a38c349c8b21d1a76ec69093","datavalue":{"value":{"entity-type":"item","numeric-id":1322846,"id":"Q1322846"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4650285$01115F2F-ACD2-42D5-AEFE-A208A8E39484","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"6218d42f0175ef35f91c4900eb5db86484a9463d","datavalue":{"value":{"entity-type":"item","numeric-id":2710590,"id":"Q2710590"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4650285$1729B74F-D2B7-40AC-912C-7BA1E7A1B9E8","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0bb430d98445fad0c07a301b258c507df3dbc1f9","datavalue":{"value":{"time":"+2005-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":"Q4650285$ADD8C64B-F06C-4731-9621-15D214950E25","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4e3d6851590db1085038e68de76e5898921f28e5","datavalue":{"value":"https://projecteuclid.org/euclid.jsl/1067620188","type":"string"},"datatype":"url"},"type":"statement","id":"Q4650285$CD5B7AE4-F6AC-4E3F-A910-2549900F7FE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P205","hash":"f52ab6483261f4d9991551c5993bc4e45487ec72","datavalue":{"value":"https://hal.inria.fr/inria-00073143/file/RR-3542.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q4650285$94FB9E8C-A5E8-4C92-B856-92E8F817A1A6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4650285$E19387FA-6F09-4A7A-8E2A-09C2DC23F4F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4650285$228102C9-0ABC-491A-971E-8D14A7DB1B60","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"bc451d7d5991403a67aa426f873071eb11ca476a","datavalue":{"value":"2133232","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4650285$1DC524D3-ABB5-47D7-8B94-6B78DFEDDB8B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q4650285$8A9F0100-907E-42D7-801C-DB5E109B2FCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7f82e5b3fddf0920d7af80635fcdd17881d7b23","datavalue":{"value":"rewrite systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q4650285$C204756A-E47A-499E-A94A-ACD4426CD75F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"18d7e8a9c2fef410a0ec0f47c6e1f03bb0f97bc1","datavalue":{"value":"first-order theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q4650285$300A66AA-1CA2-40E2-A5B0-3A264229F393","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b463632838a0c59bb39ec0f7242f8d221667ab72","datavalue":{"value":"pre-model","type":"string"},"datatype":"string"},"type":"statement","id":"Q4650285$2AFE2DE2-9B5A-4875-AAF3-C5E3EF902E1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dcfc1bc00c58245854e787073d98b7cbed7ce1ba","datavalue":{"value":"cut elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q4650285$FC5837C8-9C6B-48DC-B06F-0D4622F6136B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"50ac0247726491e51a1a9dad4fadbff313f8e488","datavalue":{"value":"simple type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q4650285$7488F14F-D91D-4CB2-9B7E-815D0E3C3FBE","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a9301974fbdbf3896f705a4c8ed840f169a9b63f","datavalue":{"value":{"entity-type":"item","numeric-id":19182,"id":"Q19182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4650285$DED1C6E4-D622-4656-848C-4472DADD2A75","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":"Q4650285$3146DDD9-8EB3-4824-B4C8-D4375C1035C9","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":"Q4650285$796297F0-036B-4A71-AD53-F7FFB8BD562C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"abdc0e550f7dcb4d7476bbd5db26952122fdc3ec","datavalue":{"value":"W1977882652","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4650285$3687E56B-7206-473C-8D9F-2C45D67D6545","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"d11e2d3338d34d0073a49be75da78015ed424a07","datavalue":{"value":{"entity-type":"item","numeric-id":4732467,"id":"Q4732467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4650285$17B2E405-DCA2-48FE-882C-CDEA7E26DDF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8124e2aa86067094dab23bb14b8dadf2e19d522b","datavalue":{"value":{"entity-type":"item","numeric-id":3894958,"id":"Q3894958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4650285$14562C1A-871C-4BC9-9E8A-753901C3AD0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ca7e027091589776f78a6d7ad8457e805c17b28","datavalue":{"value":{"entity-type":"item","numeric-id":5777498,"id":"Q5777498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4650285$B93E0FDA-2294-481E-9AEC-A52928B7EA5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d592f87e8857ff4d106dd1dd178161f50c9229b","datavalue":{"value":{"entity-type":"item","numeric-id":1108266,"id":"Q1108266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4650285$AE76B94D-AE0B-44B7-9897-4D6F68CB7AFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4c7e99dee790823bc8c804e87dda851e7f3087c6","datavalue":{"value":{"entity-type":"item","numeric-id":4365102,"id":"Q4365102"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4650285$F62A29BA-EB65-49A8-8DEB-0FD3A83C0B47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b714ee7bdb70947b555d42ec2db46670455bb12f","datavalue":{"value":{"entity-type":"item","numeric-id":1431339,"id":"Q1431339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4650285$7CB1ACF2-3FDA-40FB-9C54-8D5C6ECF3DA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bf16a30b197dd393a2021c38d09affdcbe8d7c4a","datavalue":{"value":{"entity-type":"item","numeric-id":5724308,"id":"Q5724308"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4650285$C2A008E7-BA24-4583-A351-567DC7DFFEAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5ca4f823ca2e82e86e612699cdb65f38c133999d","datavalue":{"value":{"entity-type":"item","numeric-id":4052071,"id":"Q4052071"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4650285$04870FC1-7435-493C-B0D0-27211CFC5F4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"99c6176bcb92cea3bde43c51d54f8875f446d09c","datavalue":{"value":{"entity-type":"item","numeric-id":3994895,"id":"Q3994895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4650285$1E41EC6F-94D6-48F6-A1F9-BD0ACA9353C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e49e0792644e85f0d945066220692a23ab216115","datavalue":{"value":{"entity-type":"item","numeric-id":3819063,"id":"Q3819063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4650285$EB9E31F1-ADED-4252-9755-F0CB89478F24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"85a15bfe95a60b53b4fa4d80a8444dfc5ccbed95","datavalue":{"value":{"entity-type":"item","numeric-id":5822062,"id":"Q5822062"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4650285$5C535288-3A4F-4A5C-B4F1-643340DD6043","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e9acb750b5a1fcf5fe08b591fc6df182dd9e5e0","datavalue":{"value":{"entity-type":"item","numeric-id":3883561,"id":"Q3883561"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4650285$5313E48E-9BD1-427A-9B04-4F09030380E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"36b355c034a15b6951cab8a2fb9dd01fb3be3dbf","datavalue":{"value":{"entity-type":"item","numeric-id":3477935,"id":"Q3477935"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4650285$03A5090E-7FB8-446A-8B52-43EE1C75EEC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fe2599506b761f6ddc2f9b7528edb9c1e7b0c44a","datavalue":{"value":{"entity-type":"item","numeric-id":3543645,"id":"Q3543645"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4650285$47EF4FA3-F737-4FD6-91DB-FB9BEF76A8D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f9579a4ebc8fc362938d3ee4c1626b4dbb8862f2","datavalue":{"value":{"entity-type":"item","numeric-id":4281483,"id":"Q4281483"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4650285$C42621B7-CE20-4AC6-95CF-E4CF4C0973FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"10514d04294539f6b18e653ffed15729ce3e519b","datavalue":{"value":{"entity-type":"item","numeric-id":5678447,"id":"Q5678447"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4650285$6A5230FB-4A23-4440-AFA0-443ED1B48A87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8d95625ec9e5b7c46cee42d87256157d982706a","datavalue":{"value":{"entity-type":"item","numeric-id":5559220,"id":"Q5559220"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4650285$27BE4E6E-E071-49D8-A1DB-E0F54B07C4FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"27ee3b057142576093bd9e66364057980fafc0e4","datavalue":{"value":{"entity-type":"item","numeric-id":1821564,"id":"Q1821564"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4650285$D62A5730-8B0C-4EA1-8490-3E545A0A6447","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3c7130b8e8ad403bac4e3a609004e5598d1175d3","datavalue":{"value":{"entity-type":"item","numeric-id":5561939,"id":"Q5561939"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4650285$E61074DB-16B2-46E0-8392-9BB989FB382F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"09efd7a62d5226c28497689016560e8e3ef9c307","datavalue":{"value":"10.2178/JSL/1067620188","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4650285$B40EE932-375E-45F7-B2B4-0A0BA3214C1F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cf860819a7d9e00e8ecfc66b9e54f67135b51fe0","datavalue":{"value":{"entity-type":"item","numeric-id":5111901,"id":"Q5111901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2255ee8867c2fc5d57e9e0d2b68cb283e97e8650","datavalue":{"value":{"amount":"+0.7992818355560303","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":"Q4650285$6829D01F-0CAF-4F1E-877B-71E940108A3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"af80fa7cc9c34af0874ea12b6d37b1a8c62ce0b5","datavalue":{"value":{"entity-type":"item","numeric-id":5387889,"id":"Q5387889"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ea40d3d5856fc439b395c3c3f255e01e2d82e0b4","datavalue":{"value":{"amount":"+0.787307620048523","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":"Q4650285$8281D3E1-750F-4C86-89EB-0BC5139CCF26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"73817800316d0a9e9bfda6941eff44b25b1153ab","datavalue":{"value":{"entity-type":"item","numeric-id":2752529,"id":"Q2752529"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"981c6e863e5a4ced01f17bc10cc942c5ad80addc","datavalue":{"value":{"amount":"+0.7779368162155151","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":"Q4650285$42E8EA3A-BC28-4235-83F6-A8D1A6ED0E75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b42aabe80c7ceaee77425a0f3ae595e5d1a5c589","datavalue":{"value":{"entity-type":"item","numeric-id":3007658,"id":"Q3007658"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"981c6e863e5a4ced01f17bc10cc942c5ad80addc","datavalue":{"value":{"amount":"+0.7779368162155151","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":"Q4650285$690C33A3-E22F-4F1E-A4A9-09380800ED41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f2e209d4a21f34e0a088a607f6de8d4e53ccded8","datavalue":{"value":{"entity-type":"item","numeric-id":4365102,"id":"Q4365102"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e10e5fcb7710d1311d7220d938e94ba12675971c","datavalue":{"value":{"amount":"+0.7765656113624573","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":"Q4650285$17024AC1-1A75-4675-BF9F-0F006AF6C85E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4650285","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4650285"}}}}}