A Logical Approach to Stable Domains

Research output: Contribution to journalArticle

Authors

Colleges, School and Institutes

Abstract

Building on earlier work by Guo-Qiang Zhang on disjunctive information systems, and by Thomas Ehrhard, Pasquale Malacaria, and the first author on stable Stone duality, we develop a framework of disjunctive propositional logic in which theories correspond to algebraic L-domains. Disjunctions in the logic can be indexed by arbitrary sets (as in geometric logic) but must be provably disjoint. This raises several technical issues which have to be addressed before clean notions of axiom system and theory can be defined. We show soundness and completeness of the proof system with respect to distributive disjunctive semilattices, and prove that every such semilattice arises as the Lindenbaum algebra of a disjunctive theory. Via stable Stone duality, we show how to use disjunctive propositional logic for a logical description of algebraic L-domains. (c) 2006 Elsevier B.V. All rights reserved.

Details

Original languageEnglish
Pages (from-to)124-148
Number of pages25
JournalTheoretical Computer Science
Volume368
Issue number1-2
Publication statusPublished - 5 Dec 2006