{"entities":{"Q377482":{"pageid":379249,"ns":120,"title":"Item:Q377482","lastrevid":51860048,"modified":"2026-01-20T10:12:44Z","type":"item","id":"Q377482","labels":{"en":{"language":"en","value":"A proof-search procedure for intuitionistic propositional logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6223059"}},"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":"Q377482$E4E2C07C-3170-4470-806A-0F1C68FCDB6A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1a4f68775c5927ad4689a863bfab09c3baa23137","datavalue":{"value":{"text":"A proof-search procedure for intuitionistic propositional logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q377482$31203672-8D5B-4A46-AE73-A7EAEB1D446B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c9d3bf8793ecb33d5165571ed4bbbd303fd66e5d","datavalue":{"value":"1302.03034","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q377482$02FADA26-35B8-4324-BF4D-5EF4FA1489A1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3b417081ff3600658a3025bfda3ebccf222d36d2","datavalue":{"value":{"entity-type":"item","numeric-id":174447,"id":"Q174447"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q377482$C0DA05D8-16E6-4527-A3AA-C92F39708BAA","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a0a7cd28a9f85b9c6ad57bd5bb1ae477bfe37846","datavalue":{"value":{"entity-type":"item","numeric-id":114337,"id":"Q114337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q377482$EA964168-AEBD-42D7-8FDB-42F60C45CB11","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"102ef688e1f1ee42ad21d8460f0995ebefcc5ee1","datavalue":{"value":{"time":"+2013-11-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q377482$606ED60C-117D-4CE6-8E29-6E004E7835DF","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"2a8dac09d5205e3142248c751abd2a0e4e909ac2","datavalue":{"value":"The author presents a sequent-root proof-search procedure for intuitionistic propositional logic, essentially based on Glivenko's theorem (see [\\textit{V. Glivenko}, Bull. Cl. Sci., V. S\u00e9r., Acad. R. Belg. 15, 183--188 (1929; JFM 55.0030.05)]). It is shown that, in the context of modified intuitionistic multi-succedent and classical sequent calculi, both belonging to the family of the contraction-free Kleene's G3-style calculi (see [\\textit{S. C. Kleene}, Introduction to metamathematics. Amsterdam: North-Holland Publishing Co (1952; Zbl 0047.00703)]), a sequent is provable iff the corresponding prefixed-sequent is derivable in the procedure.","type":"string"},"datatype":"string"},"type":"statement","id":"Q377482$48A4DB1F-E40D-4AC2-AD9C-EEBBF201513E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"2337f934f367559a8ee0c48540aa4d52d0fa385a","datavalue":{"value":"03B20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q377482$6C8611A3-7A68-4926-8026-E845F3D33CDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d971f250f4b60bd91da7e9350568180af141e6af","datavalue":{"value":"03F03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q377482$C83AF36E-664C-46F3-B472-9885B3D13947","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6e2ae8b1900147d15ddea62ccb5302a15ee19b5d","datavalue":{"value":"03F07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q377482$221FDCDF-F451-4BAD-BAC3-46B3B24D6C96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q377482$17738C30-0182-4DC5-A3A2-741B64DC2630","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d78ce3a1ad335fa51c6a04e89437f6880040ef8c","datavalue":{"value":"6223059","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q377482$D965E5B1-0A65-4610-938B-C8D5FAEACF65","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6722b2209aa11f991e0cccfb18f727af37bf0db0","datavalue":{"value":"propositional intuitionistic logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q377482$D559AADB-9241-421C-9A9B-178342C99906","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2c7d4aa0d3cf1745112ae7d594a2a5578f4e767f","datavalue":{"value":"sequent calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q377482$AF473B50-141E-48BD-9D07-7D932FAC97EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b8ea5a92b1759cef1a2417e84c1a0f66f66e4d2e","datavalue":{"value":"Glivenko's theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q377482$801F1A87-FB5C-470A-9CAF-A7F089241963","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"2b87c2901b1d9462aa6fffa26502c8ee861836b0","datavalue":{"value":{"entity-type":"item","numeric-id":1062052,"id":"Q1062052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q377482$0DB85AC7-2B86-44E1-9915-5132A0557621","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ae510ff9d7026cdfae7484e5c88af62cffb92c77","datavalue":{"value":{"entity-type":"item","numeric-id":21735,"id":"Q21735"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q377482$17FD8000-7C8C-4B07-B454-F4B4DAAC3295","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a22c015b3b24c1ab8096c704eef7d553cb9e52fc","datavalue":{"value":{"entity-type":"item","numeric-id":25578,"id":"Q25578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q377482$529697EB-D783-47A2-9AC2-C3B11309CB7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"824e66560bf30b02805a91f52441dbc38109d38d","datavalue":{"value":{"entity-type":"item","numeric-id":21736,"id":"Q21736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q377482$13BED9CB-8AF2-4F89-B0BC-77A779A30EB5","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":"Q377482$E2B2F5E3-4566-4227-8F6A-ED741141C353","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e28095074e0b1f9dbcee7a607742c0e81a5a2e3b","datavalue":{"value":"https://doi.org/10.1007/s00153-013-0342-y","type":"string"},"datatype":"url"},"type":"statement","id":"Q377482$5719951E-FFAD-4E36-91B7-B5ED5CBBF097","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d2bbbf1d4d96ef3477b0c1d7995e59e38047e04d","datavalue":{"value":"W2023242314","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q377482$DED76FB9-0D19-4E40-96ED-29AE0122DA74","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"39e0191015d7da12b45852de7bb2b9f939641fe3","datavalue":{"value":{"entity-type":"item","numeric-id":3442398,"id":"Q3442398"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q377482$C9CAB009-05EC-4E30-A048-BE6B12AB1A4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aa8962bf65987aa1777186fa63cd564a4df6437b","datavalue":{"value":{"entity-type":"item","numeric-id":5200030,"id":"Q5200030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q377482$D4101636-CCE3-4787-A155-A93978E2E724","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"755ba4a7f8b70eaa04400af225724e167e2ca658","datavalue":{"value":{"entity-type":"item","numeric-id":2744125,"id":"Q2744125"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q377482$F9E8C039-C7AB-48ED-8288-FB15997E3E59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a193a471d38d4f2636f0967c462d886d529dd18f","datavalue":{"value":{"entity-type":"item","numeric-id":5604436,"id":"Q5604436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q377482$377ED5CF-D514-4DBB-AAAC-07EA8B21B386","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dbe69fc028355d5cb639899e284adf226488cd64","datavalue":{"value":{"entity-type":"item","numeric-id":3541708,"id":"Q3541708"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q377482$18BBE875-A878-440B-9097-FBFD794D8803","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"598866d6fceb16a6782266b4f4edaee4180cfccd","datavalue":{"value":{"entity-type":"item","numeric-id":1575923,"id":"Q1575923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q377482$4F485C13-2368-466D-94E0-B022EA799B53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"56327724d8101cacc3d4e5b36700dc86a7feb472","datavalue":{"value":{"entity-type":"item","numeric-id":4499084,"id":"Q4499084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q377482$3B3A118D-06E3-4C39-8220-2CDC129CCE5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f2f0d7bd7291721847e88579cf9c539e3f140b71","datavalue":{"value":{"entity-type":"item","numeric-id":2751374,"id":"Q2751374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q377482$68E79BBE-EEE6-468C-A929-328AB8CA8612","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"079d26960fbad67a47fb78241cb8cbf2b682033c","datavalue":{"value":{"entity-type":"item","numeric-id":3999539,"id":"Q3999539"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q377482$0745506B-DB1E-4CD7-8CDF-2C53D368FFAF","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"be79e11fd0e08431cb9c6b055711c7e4c5c841be","datavalue":{"value":"10.1007/S00153-013-0342-Y","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q377482$66421357-A667-4A7F-8EA0-756B579D7100","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d8601f2c220e4bfc2451ac1f63f2c6d2e366e3c5","datavalue":{"value":{"entity-type":"item","numeric-id":2811589,"id":"Q2811589"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"35150276c6bad23e4c181838fcdb965c1d8e735d","datavalue":{"value":{"amount":"+0.8393796682357788","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":"Q377482$17BDEF7F-90E0-46BD-A01D-F747901D44EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9d1bff0083d5306f78d94ac28e217263fa23a329","datavalue":{"value":{"entity-type":"item","numeric-id":1725847,"id":"Q1725847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"073243ec10b3e15de60df93587a56609d2cdc432","datavalue":{"value":{"amount":"+0.816444993019104","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":"Q377482$29F99E5B-9775-40E6-974B-3FEEAF39BA3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"61bd3300c7dc67e2bc56e6bd1256442b32e9f142","datavalue":{"value":{"entity-type":"item","numeric-id":4645244,"id":"Q4645244"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f180e0312d84f5864fcc591a65d68e12fdcb5a57","datavalue":{"value":{"amount":"+0.8135802745819092","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":"Q377482$A8993C53-D676-474B-AA4A-04439DC34049","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"687c2a5c6256dd6cbca81f795852ca264521fc74","datavalue":{"value":{"entity-type":"item","numeric-id":3417780,"id":"Q3417780"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2192e29a8a8b4ac4a250c515187a049c15e3a3a2","datavalue":{"value":{"amount":"+0.8060115575790405","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":"Q377482$EC7A4828-E92F-40AF-8CC3-15D25E8ABD1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"11e9b9d0f7d471546cf959849cfb3699590e8c97","datavalue":{"value":{"entity-type":"item","numeric-id":4533383,"id":"Q4533383"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ec306992f010f8656adf74dd69f799950f95a1b1","datavalue":{"value":{"amount":"+0.801535964012146","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":"Q377482$452BA2F4-04B3-44F0-8C31-7007EBB3A4B9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:377482","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:377482"}}}}}