{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T12:38:44Z","timestamp":1740141524829,"version":"3.37.3"},"reference-count":18,"publisher":"Oxford University Press (OUP)","issue":"1","license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"funder":[{"name":"TCS Research Fellowship"},{"DOI":"10.13039\/501100007296","name":"Infosys Foundation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100007296","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020,1,23]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We study procedures for the derivability problem of fragments of intuitionistic logic. Intuitionistic logic is known to be PSPACE-complete, with implication being one of the main contributors to this complexity. In fact, with just implication alone, we still have a PSPACE-complete logic. We study fragments of intuitionistic logic with restricted implication and develop algorithms for these fragments which are based on the proof rules. We identify a core fragment whose derivability is solvable in linear time. Adding disjunction elimination to this core gives a logic which is solvable in co-NP. These sub-procedures are applicable to a wide variety of logics with rules of a similar flavour. We also show that we cannot do better than co-NP whenever disjunction elimination interacts with other rules.<\/jats:p>","DOI":"10.1093\/logcom\/exaa018","type":"journal-article","created":{"date-parts":[[2020,1,6]],"date-time":"2020-01-06T12:08:28Z","timestamp":1578312508000},"page":"421-445","source":"Crossref","is-referenced-by-count":0,"title":["The complexity of disjunction in intuitionistic logic"],"prefix":"10.1093","volume":"30","author":[{"given":"R","family":"Ramanujam","sequence":"first","affiliation":[{"name":"The Institute of Mathematical Sciences, Chennai, India - 600113"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vaishnavi","family":"Sundararajan","sequence":"first","affiliation":[{"name":"Chennai Mathematical Institute, Chennai, India - 603103"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S P","family":"Suresh","sequence":"first","affiliation":[{"name":"Chennai Mathematical Institute, Chennai, India - 603103"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2020,2,26]]},"reference":[{"key":"2020040702352623600_ref1","doi-asserted-by":"crossref","first-page":"706","DOI":"10.1145\/155183.155225","article-title":"A calculus for access control in distributed systems","volume":"15","author":"Abadi","year":"1993","journal-title":"ACM Transactions on Programming Languages and Systems"},{"volume-title":"Tonk\u2014A Full Mathematical Solution","year":"2010","author":"Avron","key":"2020040702352623600_ref2"},{"key":"2020040702352623600_ref3","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1093\/logcom\/exs018","article-title":"Propositional primal logic with disjunction","volume":"24","author":"Beklemishev","year":"2014","journal-title":"Journal of Logic and Computation"},{"key":"2020040702352623600_ref4","first-page":"163","article-title":"derivability in polynomial time","volume-title":"Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)","author":"Baskar","year":"2013"},{"key":"2020040702352623600_ref5","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1109\/LICS.2003.1210067","article-title":"Intruder deductions, constraint solving and insecurity decision in presence of exclusive or","author":"Comon-Lundh","year":"2003","journal-title":"Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003)"},{"key":"2020040702352623600_ref6","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/978-3-540-39910-0_10","article-title":"Easy intruder deductions","volume-title":"Verification: Theory and Practice","author":"Comon-Lundh","year":"2003"},{"volume-title":"Modal Logic","year":"1997","author":"Chagrov","key":"2020040702352623600_ref7"},{"key":"2020040702352623600_ref8","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","article-title":"On the security of public key protocols","volume":"29","author":"Dolev","year":"1983","journal-title":"IEEE Transactions on Information Theory"},{"key":"2020040702352623600_ref9","doi-asserted-by":"crossref","first-page":"67","DOI":"10.2307\/2272344","article-title":"A sequence of decidable finitely axiomatizable intermediate logics with the disjunction property","volume":"39","author":"Gabbay","year":"1974","journal-title":"Journal of Symbol Logic"},{"key":"2020040702352623600_ref10","first-page":"149","article-title":"DKAL: distributed-knowledge authorization language","volume-title":"21st IEEE CSF Symposium","author":"Gurevich","year":"2008"},{"key":"2020040702352623600_ref11","doi-asserted-by":"crossref","first-page":"9:1","DOI":"10.1145\/1877714.1877715","article-title":"Logic of infons: the propositional case","volume":"12","author":"Gurevich","year":"2011","journal-title":"ACM Transactions on Computational Logic"},{"key":"2020040702352623600_ref12","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1016\/j.apal.2009.07.013","article-title":"Hypersequent calculi for intuitionistic logic with classical atoms","volume":"161","author":"Kurokawa","year":"2009","journal-title":"Annals of Pure and Applied Logic"},{"key":"2020040702352623600_ref13","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1145\/151261.151265","article-title":"Automatic recognition of tractability in inference relations","volume":"40","author":"McAllister","year":"1993","journal-title":"Journal of the ACM"},{"key":"2020040702352623600_ref14","doi-asserted-by":"crossref","first-page":"536","DOI":"10.1016\/j.ipl.2015.01.003","article-title":"The complexity of primal logic with disjunction","volume":"115","author":"Magirius","year":"2015","journal-title":"Information Processing Letters"},{"key":"2020040702352623600_ref15","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/978-3-319-13841-1_4","article-title":"Extending Dolev\u2013Yao with assertions","volume-title":"The 10th International Conference on Information Systems Security","author":"Ramanujam","year":"2014"},{"key":"2020040702352623600_ref16","first-page":"337","article-title":"Existential assertions for voting protocols","volume-title":"Proceedings of Financial Cryptography 2017 Workshops (Voting \u201917)","author":"Ramanujam","year":"2017"},{"volume-title":"Median logic","year":"2004","author":"Sakharov","key":"2020040702352623600_ref17"},{"key":"2020040702352623600_ref18","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0304-3975(79)90006-9","article-title":"Intuitionistic propositional logic is polynomial-space complete","volume":"9","author":"Statman","year":"1979","journal-title":"Theoretical Computer Science"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/30\/1\/421\/33016558\/exaa018.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/30\/1\/421\/33016558\/exaa018.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,24]],"date-time":"2023-09-24T19:36:34Z","timestamp":1695584194000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/30\/1\/421\/5754082"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1]]},"references-count":18,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2020,2,26]]},"published-print":{"date-parts":[[2020,1,23]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exaa018","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"type":"print","value":"0955-792X"},{"type":"electronic","value":"1465-363X"}],"subject":[],"published-other":{"date-parts":[[2020,1]]},"published":{"date-parts":[[2020,1]]}}}