{"entities":{"Q5089014":{"pageid":7118590,"ns":120,"title":"Item:Q5089014","lastrevid":55415311,"modified":"2026-02-17T15:57:10Z","type":"item","id":"Q5089014","labels":{"en":{"language":"en","value":"Proof normalisation in a logic identifying isomorphic propositions"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7559280"}},"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":"Q5089014$A6589748-5150-46C4-9800-24FC213097B5","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4d46858b2e681b050e11340ef98cbddcf45ff298","datavalue":{"value":{"entity-type":"item","numeric-id":529048,"id":"Q529048"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089014$944CC55B-BBDE-4D0D-AB76-2BB124FD3577","rank":"normal"},{"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":"Q5089014$D069D207-6E22-48AF-8AD1-31541F1B81FD","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6793430fc5b4ace9180691774574e339423361ba","datavalue":{"value":{"time":"+2022-07-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5089014$4F2792BB-E829-4733-B106-FCA217B7AC6D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8a4bc2270cd9b97a20dd2967bfc83032759291d6","datavalue":{"value":"https://arxiv.org/abs/1501.06125","type":"string"},"datatype":"url"},"type":"statement","id":"Q5089014$A05751BA-CA50-488C-95FB-0D98D5B5D4B4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5089014$D7B476F1-DAB6-482A-8C06-32F34076E2FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f969879f531643f058f8dd4c87a7dd4eb7b8c4c8","datavalue":{"value":"68Qxx","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5089014$A7F91B9D-E2E3-4ED0-9FF2-1C904B1F4C31","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b70e189ccf84cfd7fdd0602464a80e7b6888229c","datavalue":{"value":"7559280","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5089014$5B20C634-12B9-4C37-87AC-3AAFBF3D5EDF","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"35fc162c76af7b869d64998d128aab85c0c79ee5","datavalue":{"value":"simply typed \\(\\lambda\\) calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q5089014$6A828064-3290-445D-96E9-D515EC8B6130","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2e205918ef9e9725c5b434cb4e8cdf1835fe6252","datavalue":{"value":"isomorphisms","type":"string"},"datatype":"string"},"type":"statement","id":"Q5089014$81805658-1348-4206-9269-8B5E7927E406","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4bbb0c1d4a0dde26226934f7234d049627289106","datavalue":{"value":"logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5089014$330186B5-2537-4D08-BA60-4E3E11ACC28B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ee0a69ba46a5f23ccf6ad83fcf01b7501a19fa4e","datavalue":{"value":"cut-elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q5089014$39FDB5F4-AF9E-43B4-B05F-FCE370EA31A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"69d16c34de29f379f44f4db883438e7b660d0a4c","datavalue":{"value":"proof-reduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q5089014$8F98C81D-803C-4B77-806B-BCAC8D1B327E","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":"Q5089014$A67082E8-96DB-4D1C-A432-16C8FA532811","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd8fe2097d6a43ae9325a34d980fac0b22e147c2","datavalue":{"value":{"entity-type":"item","numeric-id":2881078,"id":"Q2881078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089014$A27A894C-9709-4554-AD68-B57B3A4EC194","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d954d0bd9f4f0e8641f1df7607608bbeec9d34ac","datavalue":{"value":{"entity-type":"item","numeric-id":529049,"id":"Q529049"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089014$77063D92-9FF4-4928-8DE4-9C3174C4FEB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4c4f020a51168a828551c25efe2435d5943ef4dc","datavalue":{"value":{"entity-type":"item","numeric-id":3522006,"id":"Q3522006"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089014$7F35E552-316A-4738-B677-50A03A795D21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aa641d9bd95d099beb13e931a65ef0f86bf7dfcd","datavalue":{"value":{"entity-type":"item","numeric-id":2980972,"id":"Q2980972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089014$0573935D-AB99-48D1-925A-4059A28A5718","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"afa831f2062bd418316f0ddf8d55a39363b94c1f","datavalue":{"value":{"entity-type":"item","numeric-id":1314269,"id":"Q1314269"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089014$0B9DC116-0722-4442-B6D6-AB54077C1DD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"308895c836b930be70b0ca58cc1956e776eb29fa","datavalue":{"value":{"entity-type":"item","numeric-id":4017461,"id":"Q4017461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089014$F0E335D3-EC38-4571-8750-E20C7D24F283","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"152529a731a5e87e191e763c50e57d59c2145e8a","datavalue":{"value":{"entity-type":"item","numeric-id":408545,"id":"Q408545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089014$01B52792-5813-4DC0-B580-4E7122BEDCD1","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":"Q5089014$FBC4BC50-DDF9-4269-8F45-F7B5BE5495EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aeae088c411532f7940546bb53e5a8a76f6e4b04","datavalue":{"value":{"entity-type":"item","numeric-id":2508325,"id":"Q2508325"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089014$B041226D-1BED-4C8B-903D-29910A53A999","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1bc37ebf85b158f95e7a2fe63513f109810e5d01","datavalue":{"value":{"entity-type":"item","numeric-id":4210114,"id":"Q4210114"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089014$113583F0-B42C-4F56-AF0F-2C65DD12B31F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ef2139b24faac29260605061d8111231a2904d6c","datavalue":{"value":{"entity-type":"item","numeric-id":4325974,"id":"Q4325974"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089014$2A115794-CAA4-4B74-8DAE-C833BB22E54F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8bb2a4f0603188267aa3fd0208ee45953e029cb","datavalue":{"value":{"entity-type":"item","numeric-id":3372683,"id":"Q3372683"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089014$24F4ECD8-A744-4EE8-A73F-864A33A9E140","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7d3687c6e4eceb35d11ec583de1ffd8ff2c143cb","datavalue":{"value":{"entity-type":"item","numeric-id":4992399,"id":"Q4992399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089014$6C91AAC1-ACAD-4389-916B-9034B6C8F09C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4d274fd939869bd955ebc1c14db907af76cff4a9","datavalue":{"value":{"entity-type":"item","numeric-id":2915029,"id":"Q2915029"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089014$276EEA49-ED8C-4833-B290-CF5C0E56B68E","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":"Q5089014$571F1F00-24CA-4A2C-A82E-8CCAEEE3066B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77a1539bff2c004078e670cfe2b9c31fd715aeff","datavalue":{"value":{"entity-type":"item","numeric-id":719245,"id":"Q719245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089014$D91CB2B8-D72C-48D0-828A-D76876DF3BBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e52f792aed007740441efa3e7b7b70e2d7b6c5c","datavalue":{"value":{"entity-type":"item","numeric-id":4650285,"id":"Q4650285"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089014$C20BEDDB-214F-4460-B8D5-64CB6776F791","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":"Q5089014$959DAB5C-9B78-4C50-B45B-8DED2FC9CD17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47b0ec3118c55b6f3ab232f29debefc8c9d383a9","datavalue":{"value":{"entity-type":"item","numeric-id":3688389,"id":"Q3688389"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089014$D81BDAF4-314E-4306-93D6-2E9DA4A9D7C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"28494d20396af22c610619948e85664efe1fa4b5","datavalue":{"value":{"entity-type":"item","numeric-id":3000282,"id":"Q3000282"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089014$74F6F66B-9DF7-4E79-8068-9F42CD01C195","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5f088588b08bc91ef8e88a52d0bd8f16267eea4e","datavalue":{"value":{"entity-type":"item","numeric-id":2352491,"id":"Q2352491"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089014$466A78E6-8D9E-4080-A715-F2DFCA9CF58C","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":"Q5089014$432CE76E-4B69-44D5-8092-9D7379786208","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5eb4a9e70f21c6dfe8888ca8944df9d2ab9a557","datavalue":{"value":{"entity-type":"item","numeric-id":3643363,"id":"Q3643363"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089014$0B9F0551-50BB-4F3F-BFCA-726305AD9BB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eec1396a43e040fa9655847cc89b616307ddbcc7","datavalue":{"value":{"entity-type":"item","numeric-id":6488563,"id":"Q6488563"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089014$540A1317-14FC-4AAC-BE14-4A56D5FAB71F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c5e409ac02431ce44c5be0c18e34c6527b818048","datavalue":{"value":"10.4230/LIPICS.FSCD.2019.14","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5089014$45F21431-816E-402E-8FE1-5BF304A49572","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"693a42c13d14166cbea12d11a5c153d2ecc42079","datavalue":{"value":{"entity-type":"item","numeric-id":3117775,"id":"Q3117775"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"47bdbe174cbdcd09b4f36215b0b7c4b0d4a97444","datavalue":{"value":{"amount":"+0.7721765041351318","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":"Q5089014$32777770-14D5-4698-9B55-1BD8144A0AC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"53b0fb8e7afe5135047663860d6ab6e199edbbe3","datavalue":{"value":{"entity-type":"item","numeric-id":4944850,"id":"Q4944850"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"86bcaa910f5b30954bd369e59fadf14cad7b219a","datavalue":{"value":{"amount":"+0.7275505661964417","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":"Q5089014$19B1C33B-7336-4246-AE95-C5BDDE436760","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4fd43aeb7e077e004a58f71e8c65c70e807b2737","datavalue":{"value":{"entity-type":"item","numeric-id":6060676,"id":"Q6060676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6a56cdbe9a2d8afe0641702151d0f415a6aea7f4","datavalue":{"value":{"amount":"+0.7259761691093445","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":"Q5089014$E1F3D2A4-92C5-4D6F-B6CA-8A518E0D31F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"62d0950f3b1226e6997e75c70690bc4d4b1bcced","datavalue":{"value":{"entity-type":"item","numeric-id":4650310,"id":"Q4650310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"095e03c46fd249c4496e3e9fb706ae9ede919a74","datavalue":{"value":{"amount":"+0.7254786491394043","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":"Q5089014$5ABDD4E7-4EE0-4C8F-A0D7-BC0C1BA29D5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"063ad9599fb8fe9d6fbb4fc834f6db6a095f0144","datavalue":{"value":{"entity-type":"item","numeric-id":4010353,"id":"Q4010353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"22bfd72700818f04b056d7c553df9a27818fb921","datavalue":{"value":{"amount":"+0.718176543712616","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":"Q5089014$8BA63315-8DD3-4BB4-9815-1965B9B8FF60","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5089014","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5089014"}}}}}