2015/02/19 by Raine Rönnholm, Rönnholm, Raine
Computer Science · #Distributed systems and fault tolerance #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge
paper · pdf · doi:10.48550/arxiv.1502.05632
openalex publication_date 2015/02/19 · openalex created_date 2022/10/05 · openalex updated_date 2026/07/28
In this paper we analyze k-ary inclusion-exclusion logic, INEX[k], which is\nobtained by extending first order logic with k-ary inclusion and exclusion\natoms. We show that every formula of INEX[k] can be expressed with a formula of\nk-ary existential second order logic, ESO[k]. Conversely, every formula of\nESO[k] with at most k-ary free relation variables can be expressed with a\nformula of INEX[k]. From this it follows that, on the level of sentences,\nINEX[k] captures the expressive power of ESO[k].\n We also introduce several useful operators that can be expressed in INEX[k].\nIn particular, we define inclusion and exclusion quantifiers and so-called term\nvalue preserving disjunction which is essential for the proofs of the main\nresults in this paper. Furthermore, we present a novel method of relativization\nfor team semantics and analyze the duality of inclusion and exclusion atoms.\n