TRANSITIVE PRIMAL INFON LOGIC.
Primal infon logic was introduced in 2009 in connection with access control. In addition to traditional logic constructs, it contains unary connectives p said indispensable in the intended access control applications. Propositional primal infon logic is decidable in linear time, yet suffices for man...
| Publicado en: | Review of Symbolic Logic Vol. 6; no. 2; pp. 281 - 305 |
|---|---|
| Autores principales: | , |
| Formato: | Artículo |
| Publicado: |
Cambridge University Press
Jun2013
|
| Materias: | |
| Acceso en línea: | Ver este registro en EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=87713621&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 87713621 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 17550203 8OI1 jtl: Review of Symbolic Logic issn: 17550203 maglogo: N pubinfo: dt: Jun2013 vid: 6 iid: 2 pid: 15979 pub: Cambridge University Press artinfo: ui: 87713621 10.1017/S1755020312000366 ppf: 281 ppct: 24 formats: tig: atl: TRANSITIVE PRIMAL INFON LOGIC. aug: au: COTRINI, CARLOS GUREVICH, YURI affil: Swiss Federal Institute of Technology Microsoft Research su: Access control Application software Mathematics theorems Algorithms Mathematical formulas Axioms sug: subj: Access control Application software Mathematics theorems Algorithms Mathematical formulas Axioms ab: Primal infon logic was introduced in 2009 in connection with access control. In addition to traditional logic constructs, it contains unary connectives p 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: $x \to y$ and $y \to z$ do not necessarily yield $x \to z$. Here we introduce and investigate equiexpressive “transitive” extensions TPIL and TPIL* of propositional primal infon logic as well as their quote-free fragments TPIL0 and TPIL0* respectively. We prove the subformula property for TPIL0* 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*. pubtype: Academic Journal doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y dt: @attributes: year: 2013 holdings: @attributes: islocal: N |
|---|