{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T09:43:33Z","timestamp":1742636613152},"reference-count":27,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2013,3,21]],"date-time":"2013-03-21T00:00:00Z","timestamp":1363824000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["The Review of Symbolic Logic"],"published-print":{"date-parts":[[2013,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Primal infon logic was introduced in 2009 in connection with access control. In addition to traditional logic constructs, it contains unary connectives <jats:italic>p<\/jats:italic> said indispensable in the intended access control applications. Propositional primal infon logic is decidable in linear time, yet suffices for many common access control scenarios. The most obvious limitation on its expressivity is the failure of the transitivity law for implication: <jats:inline-formula><jats:alternatives><jats:graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" orientation=\"portrait\" mime-subtype=\"gif\" mimetype=\"image\" position=\"float\" xlink:type=\"simple\" xlink:href=\"S1755020312000366_inline1\" \/><jats:tex-math>$x \\to y$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> and <jats:inline-formula><jats:alternatives><jats:graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" orientation=\"portrait\" mime-subtype=\"gif\" mimetype=\"image\" position=\"float\" xlink:type=\"simple\" xlink:href=\"S1755020312000366_inline2\" \/><jats:tex-math>$y \\to z$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> do not necessarily yield <jats:inline-formula><jats:alternatives><jats:graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" orientation=\"portrait\" mime-subtype=\"gif\" mimetype=\"image\" position=\"float\" xlink:type=\"simple\" xlink:href=\"S1755020312000366_inline3\" \/><jats:tex-math>$x \\to z$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>. Here we introduce and investigate equiexpressive \u201ctransitive\u201d extensions TPIL and TPIL* of propositional primal infon logic as well as their quote-free fragments TPIL<jats:sub>0<\/jats:sub> and TPIL<jats:sub>0<\/jats:sub>* respectively. We prove the subformula property for TPIL<jats:sub>0<\/jats:sub>* and a similar property for TPIL*; we define Kripke models for the four logics and prove the corresponding soundness-and-completeness theorems; we show that, in all these logics, satisfiable formulas have small models; but our main result is a quadratic-time derivation algorithm for TPIL*.<\/jats:p>","DOI":"10.1017\/s1755020312000366","type":"journal-article","created":{"date-parts":[[2013,3,21]],"date-time":"2013-03-21T15:33:02Z","timestamp":1363879982000},"page":"281-304","source":"Crossref","is-referenced-by-count":6,"title":["TRANSITIVE PRIMAL INFON LOGIC"],"prefix":"10.1017","volume":"6","author":[{"given":"CARLOS","family":"COTRINI","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"YURI","family":"GUREVICH","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2013,3,21]]},"reference":[{"key":"S1755020312000366_ref2","unstructured":"Beklemishev L. , Blass A. , & Gurevich Y. What is the logic of information? In preparation."},{"key":"S1755020312000366_ref1","first-page":"62","article-title":"Canonical constructive systems","volume":"2009","author":"Avron","year":"2009","journal-title":"Proceedings of TABLEAUX"},{"key":"S1755020312000366_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-2109-7_17"},{"key":"S1755020312000366_ref3","article-title":"Propositional primal logic with disjunction","author":"Beklemishev","year":"2012","journal-title":"Journal of Logic and Computation"},{"key":"S1755020312000366_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(88)90124-X"},{"key":"S1755020312000366_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995108"},{"key":"S1755020312000366_ref12","unstructured":"Fortnow, L. (2009). Shaving logs with unit cost. http:\/\/blog.computationalcomplexity.org\/2009\/05\/shaving-logs-with-unit-cost.html, seen July 22, 2012."},{"key":"S1755020312000366_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30743-0_6"},{"key":"S1755020312000366_ref14","volume-title":"Two Notes on Propositional Primal Logic","author":"Gurevich","year":"2011"},{"key":"S1755020312000366_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(84)90014-1"},{"key":"S1755020312000366_ref8","article-title":"Basic primal infon logic","author":"Cotrini","year":"2013","journal-title":"Journal of Logic and Computation"},{"key":"S1755020312000366_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/502807.502810"},{"key":"S1755020312000366_ref25","unstructured":"Visser A. (2012). Personal communication, January 7, 2012."},{"key":"S1755020312000366_ref5","first-page":"122","article-title":"Hilbertian deductive systems, infon logic, and datalog","volume":"102","author":"Blass","year":"2010","journal-title":"Bulletin of the EATCS"},{"key":"S1755020312000366_ref6","first-page":"77","volume-title":"The Future of Software Engineering","author":"Blass","year":"2011"},{"key":"S1755020312000366_ref7","volume-title":"Introduction to Algorithms","author":"Cormen","year":"2001"},{"key":"S1755020312000366_ref10","unstructured":"DKAL at CodePlex. http:\/\/dkal.codeplex.com\/, viewed August 10, 2012."},{"key":"S1755020312000366_ref13","volume-title":"Many-dimensional Modal Logics: Theory and Applications","author":"Gabbay","year":"2003"},{"key":"S1755020312000366_ref15","first-page":"149","volume-title":"Proceedings of CSF 2008","author":"Gurevich","year":"2008"},{"key":"S1755020312000366_ref16","unstructured":"Gurevich Y. , & Neeman I. (2009). DKAL 2 \u2014 A simplified and improved authorization language. Microsoft Research Tech Report MSR-TR-2009-11, February 2009."},{"key":"S1755020312000366_ref17","article-title":"Infon logic: the propositional case","volume":"12","author":"Gurevich","year":"2011","journal-title":"ACM Transactions on Computation Logic"},{"key":"S1755020312000366_ref20","article-title":"On P\/NP dichotomies for EL subsumption under relational constraints","author":"Kurucz","year":"2011","journal-title":"Proceedings of DL 2011"},{"key":"S1755020312000366_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(95)00018-A"},{"key":"S1755020312000366_ref19","first-page":"271","volume-title":"Advances in Modal Logic","volume":"8","author":"Kurucz","year":"2010"},{"key":"S1755020312000366_ref23","volume-title":"Investigation of Primal Logic","author":"Savateev","year":"2009"},{"key":"S1755020312000366_ref24","volume-title":"Logic and Structure","author":"van Dalen","year":"2008"},{"key":"S1755020312000366_ref26","volume-title":"Logic Group Preprint Series","volume":"111","author":"Visser","year":"2008"}],"container-title":["The Review of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1755020312000366","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T21:33:47Z","timestamp":1556055227000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1755020312000366\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,3,21]]},"references-count":27,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,6]]}},"alternative-id":["S1755020312000366"],"URL":"https:\/\/doi.org\/10.1017\/s1755020312000366","relation":{},"ISSN":["1755-0203","1755-0211"],"issn-type":[{"value":"1755-0203","type":"print"},{"value":"1755-0211","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,3,21]]}}}