{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,17]],"date-time":"2026-01-17T04:11:39Z","timestamp":1768623099990,"version":"3.49.0"},"reference-count":17,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2011,1]]},"abstract":"<jats:p>\n            Infons are statements viewed as containers of information (rather then representations of truth values). The logic of infons turns out to be a conservative extension of logic known as constructive or intuitionistic. Distributed Knowledge Authorization Language uses additional unary connectives \u201c\n            <jats:italic>p<\/jats:italic>\n            said\u201d and \u201c\n            <jats:italic>p<\/jats:italic>\n            implied\u201d where\n            <jats:italic>p<\/jats:italic>\n            ranges over principals. Here we investigate infon logic and a narrow but useful\n            <jats:italic>primal<\/jats:italic>\n            fragment of it. In both cases, we develop model theory and analyze the derivability problem: Does the given query follow from the given hypotheses? Our more involved technical results are on primal infon logic. We construct an algorithm for the multiple derivability problem: Which of the given queries follow from the given hypotheses? Given a bound on the quotation depth of the hypotheses, the algorithm runs in linear time. We quickly discuss the significance of this result for access control.\n          <\/jats:p>","DOI":"10.1145\/1877714.1877715","type":"journal-article","created":{"date-parts":[[2011,1,25]],"date-time":"2011-01-25T19:12:52Z","timestamp":1295982772000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["Logic of infons"],"prefix":"10.1145","volume":"12","author":[{"given":"Yuri","family":"Gurevich","sequence":"first","affiliation":[{"name":"Microsoft Research, Redmond, WA"}]},{"given":"Itay","family":"Neeman","sequence":"additional","affiliation":[{"name":"UCLA, Los Angeles, CA"}]}],"member":"320","published-online":{"date-parts":[[2011,1,27]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Hues of Philosophy: Essays in Memory of Ruth Manor, Ed. A. Biletzki","author":"Avron A."},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Avron A.\n     and \n      \n      \n      Lahav O\n      \n  \n  . \n  2009\n  . Strict canonical constructive systems. In Fields of Logic and Computation: Essays Dedicated to Yuri Gurevich on the Occasion of his 70th Birthday Eds. A. Blass N. Dershowitz and W. Reisig Lecture Notes in Computer Science vol. \n  6300 Springer-Verlag 75--94.   Avron A. and Lahav O. 2009. Strict canonical constructive systems. In Fields of Logic and Computation: Essays Dedicated to Yuri Gurevich on the Occasion of his 70 th Birthday Eds. A. Blass N. Dershowitz and W. Reisig Lecture Notes in Computer Science vol. 6300 Springer-Verlag 75--94.","DOI":"10.1007\/978-3-642-15025-8_4"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2007.18"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-009-9201-6"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00183-J"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322243"},{"key":"e_1_2_1_7_1","unstructured":"Cormen T. H. Leiserson C. E. and Rivest R. L. 1990. Algorithms. MIT Press.  Cormen T. H. Leiserson C. E. and Rivest R. L. 1990. Algorithms. MIT Press."},{"key":"e_1_2_1_8_1","unstructured":"Devlin K. 1991. Logic and Information. Cambridge University Press.   Devlin K. 1991. Logic and Information. Cambridge University Press."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2008.8"},{"key":"e_1_2_1_10_1","unstructured":"Gurevich Y. and Neeman I. 2009. DKAL 2\u2014A simplified and improved authorization language. Tech. rep. MSR-TR-2009-11 Microsoft Research.  Gurevich Y. and Neeman I. 2009. DKAL 2\u2014A simplified and improved authorization language. Tech. rep. MSR-TR-2009-11 Microsoft Research."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03748-1_15"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(92)90049-4"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Kripke S. 1965. Semantical analysis of intuitionistic logic I. In Formal Systems and Recursive Functions J. W. Addison L. Henkin and A. Tarski Eds. North-Holland.  Kripke S. 1965. Semantical analysis of intuitionistic logic I. In Formal Systems and Recursive Functions J. W. Addison L. Henkin and A. Tarski Eds. North-Holland.","DOI":"10.1016\/S0049-237X(08)71685-9"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Ladner R. E. 1977. The computational complexity of provability in systems of modal propositional logic. Siam J. Comput. 467--480.  Ladner R. E. 1977. The computational complexity of provability in systems of modal propositional logic. Siam J. Comput. 467--480.","DOI":"10.1137\/0206033"},{"key":"e_1_2_1_15_1","unstructured":"Mints G. 2000. A Short Introduction to Intuitionist Logic. Kluwer.   Mints G. 2000. A Short Introduction to Intuitionist Logic. Kluwer."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1462179.1462185"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Statman R. 1979. Intuitionistic propositional logic is polynomial-space complete. Theor. Comput. Sci. 67--72.  Statman R. 1979. Intuitionistic propositional logic is polynomial-space complete. Theor. Comput. Sci. 67--72.","DOI":"10.1016\/0304-3975(79)90006-9"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1877714.1877715","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1877714.1877715","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:17:36Z","timestamp":1750249056000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1877714.1877715"}},"subtitle":["The propositional case"],"short-title":[],"issued":{"date-parts":[[2011,1]]},"references-count":17,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,1]]}},"alternative-id":["10.1145\/1877714.1877715"],"URL":"https:\/\/doi.org\/10.1145\/1877714.1877715","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,1]]},"assertion":[{"value":"2009-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-01-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}