{"entities":{"Q2655331":{"pageid":2666074,"ns":120,"title":"Item:Q2655331","lastrevid":44579661,"modified":"2025-11-24T01:35:10Z","type":"item","id":"Q2655331","labels":{"en":{"language":"en","value":"Procedural representation of CIC proof terms"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5662162"}},"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":"Q2655331$81C45630-8966-4F3A-8E0F-B5C2D1405ED9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fa6ab89c8c74c286d24467e581c445220b266cc1","datavalue":{"value":{"text":"Procedural representation of CIC proof terms","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2655331$30981EB8-A1D4-4098-B9B7-2307DA6A1B17","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b470b20abb23f058f1edbfcad78b8f8f2d9bce59","datavalue":{"value":"1185.68622","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2655331$855D6F10-468F-420B-8D02-1516A2464052","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6f9740203aefff41b182d94540a09e0a78f60d61","datavalue":{"value":{"entity-type":"item","numeric-id":1810902,"id":"Q1810902"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2655331$6F59D10E-6F05-448F-AE75-1DD23E5004D9","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2655331$27641929-288E-432E-9BE4-CA26DCBBB59F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"eeda675146eaac960e312504b1b7dd784f800a08","datavalue":{"value":{"time":"+2010-01-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2655331$09E46220-CEE0-4D94-9065-CA310D3574B9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2655331$FC09EC10-BFBB-465D-8DD1-0C3AC26A99A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2655331$B315A606-143F-4699-A664-A2FEC99B2B3C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e7655c5bd9b2c67534951092c52e3fd0f06308d5","datavalue":{"value":"5662162","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2655331$D3DE97C0-77AD-4FD1-9D35-E028AC95D126","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aacdd9e6b1e081b5de4688ca768accb91a2c66bc","datavalue":{"value":"calculus of constructions","type":"string"},"datatype":"string"},"type":"statement","id":"Q2655331$28743847-91AB-4291-8DB7-72FC3684A69A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2e1f66f838ab6c659c40577faeda90140c2435bc","datavalue":{"value":"proof terms","type":"string"},"datatype":"string"},"type":"statement","id":"Q2655331$2808D5F5-3846-49CD-A25F-5A11ED6F711B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6180ee4c8889725a05c633e717a0765af1636d20","datavalue":{"value":"procedural proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q2655331$8AC120DF-5702-41D7-86C2-36DCF8661CF5","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e262f47aa23786f0d5ca3c491b5060c53e80792f","datavalue":{"value":{"entity-type":"item","numeric-id":18274,"id":"Q18274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2655331$26FF98B9-7D56-4888-806C-5012EBA22D10","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":"Q2655331$34F03ED7-E8C2-4CD5-A967-889F724B9187","rank":"normal"},{"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":"Q2655331$362B771E-0D72-453C-BDB0-7E6CBB4D0469","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":"Q2655331$1B17C0D7-4A11-48B7-BFDB-29DA76EAAB70","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"99212d5a379d697b3589be4c15bef0229a4abf9e","datavalue":{"value":"https://doi.org/10.1007/s10817-009-9137-6","type":"string"},"datatype":"url"},"type":"statement","id":"Q2655331$CFAB2F28-4B51-47A4-8637-D6EFCA36D059","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"4c026195a222873f67ac436e3a6aaecf9e37cfd9","datavalue":{"value":"W2100997280","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2655331$3EED8D61-7DCB-4E7E-81EA-16812A01D9EB","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c8847fc96bd6cc15667c599e80d53cc2bce3050","datavalue":{"value":{"entity-type":"item","numeric-id":2462635,"id":"Q2462635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2655331$C460F16A-E7CF-4D4E-80D3-5FA458A72BBD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"30847192b0865f8e5a0b1c2439c278e0c50d1e85","datavalue":{"value":{"entity-type":"item","numeric-id":2946591,"id":"Q2946591"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2655331$084BCAE7-FCE6-4BE5-811B-F1F1F1B6DE72","rank":"normal"},{"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":"Q2655331$5002D3C7-0222-42D8-BE1B-847A696EE36E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5193e6a5a3c0a2fde95ed5212e577b55eaa533fa","datavalue":{"value":{"entity-type":"item","numeric-id":4413879,"id":"Q4413879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2655331$30D898DF-2B92-44BB-B472-F772A2DB4EE8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"541bc36e9357802534d1e52134710ec758d76fb7","datavalue":{"value":{"entity-type":"item","numeric-id":5753923,"id":"Q5753923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2655331$F64B076E-72E9-4749-8B3E-624B48FA1834","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47cc5718e35e57ae39d15c74967403e17f65b36d","datavalue":{"value":{"entity-type":"item","numeric-id":1887432,"id":"Q1887432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2655331$352B2331-B7FC-4BF2-A0DA-3E5D50A03B3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a774592121362aea0b18362b2a1fe30f87c72aa","datavalue":{"value":{"entity-type":"item","numeric-id":1810904,"id":"Q1810904"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2655331$8D538DE3-181B-4F2C-A215-CA4B032C8B43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7b7bb7c39279605d0be633aee89b69bf2719cf19","datavalue":{"value":{"entity-type":"item","numeric-id":5898523,"id":"Q5898523"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2655331$F8AC5AA8-392F-4519-A9E5-61F3C6A2CFD4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"616aae32ef3c0d4e6b19fe90651d1ba0d66688fd","datavalue":{"value":{"entity-type":"item","numeric-id":4370238,"id":"Q4370238"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2655331$AFF91229-0F34-429B-8B5E-048FE98C4ED5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d9cb318559b5e8b835fb9fc7ea1d7ddb2a0c1f9c","datavalue":{"value":{"entity-type":"item","numeric-id":5718565,"id":"Q5718565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2655331$F5A332FA-8EB0-4EF8-93BC-8D8630AE6037","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5a5928533f1a1251f0d11dc18c7b4ce473f48af9","datavalue":{"value":{"entity-type":"item","numeric-id":4187337,"id":"Q4187337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2655331$26914D20-5F1C-48CB-8281-BE4F0C33ABA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8513d5f9fd03c9a6787159234040414ea0547c1d","datavalue":{"value":{"entity-type":"item","numeric-id":2655331,"id":"Q2655331"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2655331$31FB67B4-C785-431B-89D6-020F9553FD90","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4e2632f4636c06fa411471d9dcdabbdbe5529281","datavalue":{"value":"10.1007/S10817-009-9137-6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2655331$890DF1C0-AE45-4DD9-A885-7A18A4D197DB","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4f728407adedd518fc5b29d93b87e53f6b803cf6","datavalue":{"value":{"entity-type":"item","numeric-id":2655330,"id":"Q2655330"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"72b403d1953946b7ec175f8e57a617ace79a1dca","datavalue":{"value":{"amount":"+0.8767373","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2655331$137E6EEF-2E53-4419-80E7-ABEE7BD72999","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a4acd4389ae9e81c79b41623f1c508d68604a69d","datavalue":{"value":{"entity-type":"item","numeric-id":6160752,"id":"Q6160752"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0fa7dbd6179c670b3301cc1a57ce5401c0880da8","datavalue":{"value":{"amount":"+0.8373449","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2655331$991F924C-536F-4596-B4CC-1CB4F257FFE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5e29c3fb1f60a011e046a3a041f7bafe2b70842e","datavalue":{"value":{"entity-type":"item","numeric-id":1924823,"id":"Q1924823"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a0ca9148bffeb6391ccabf9d7daa8a1c146797cd","datavalue":{"value":{"amount":"+0.82966316","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2655331$7BB751D8-723B-4699-9217-28E58E90CDD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bedf41f4ad814a262dc70d8faa9745816259d7c9","datavalue":{"value":{"entity-type":"item","numeric-id":3189830,"id":"Q3189830"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0a665b93b0fbaea6528596dc298c1b41148fbd43","datavalue":{"value":{"amount":"+0.8262614","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2655331$7ACDC501-0516-4E70-B49F-AE831F8C1BDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e3291d51f91ffa99d748f859f093a3ddfaa21724","datavalue":{"value":{"entity-type":"item","numeric-id":5472879,"id":"Q5472879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ee19eb05d10e9ee686a9cacabf699486ff938854","datavalue":{"value":{"amount":"+0.82440686","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2655331$45A4A4E9-CB83-4373-B353-F32092FB4727","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"79dcc09fce2f4a780ce364fde69cdf04cb02acba","datavalue":{"value":{"entity-type":"item","numeric-id":5308096,"id":"Q5308096"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4d753a53f88d6526adb0920ab0a26975acf9df43","datavalue":{"value":{"amount":"+0.8234129","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2655331$5F3B4FF3-78A1-40E1-9138-8436F86C9A56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"54fd74f668204d6d27440d14dfd39de5c9ec904a","datavalue":{"value":{"entity-type":"item","numeric-id":3382810,"id":"Q3382810"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dda420881b5ab1f30a9d5b2371c1421950b3672f","datavalue":{"value":{"amount":"+0.81622404","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2655331$D3343BAF-3E7C-49BB-8D51-0E8EF1752FEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b8a5d18780a3dbdb4959fbe9fb76a2b4792c26e8","datavalue":{"value":{"entity-type":"item","numeric-id":3490999,"id":"Q3490999"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d5fd36507eb1e8e59b3596c19c9e38a52fa64d69","datavalue":{"value":{"amount":"+0.8162124","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2655331$45FF658B-1C0E-44D1-9737-561B5E39063A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d43c8caecbde7694f12ec3164da9e4d96d586bac","datavalue":{"value":{"entity-type":"item","numeric-id":693063,"id":"Q693063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"42c7cda49d7e7893a14f0fc10a51e4738b7ffc05","datavalue":{"value":{"amount":"+0.8160802","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2655331$B477DA15-740F-4E3D-AEF6-A71EE3698695","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2655331","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2655331"}}}}}