A representation of proper BC domains based on conjunctive sequent calculi
A representation of proper BC domains based on conjunctive sequent calculi
复制标题
基于合取顺序演算的真 BC 域的表示
DOI：
10.1017/s096012951900015x
复制
发表时间：
2019-10
影响因子：
0.5
通讯作者：
Li Qingguo
中科院分区：
文献类型：
--
作者：
Wang Longchun;Li Qingguo
摘要我们建立了一个逻辑系统--合取命题演算，它是经典命题演算在证明论意义下的合取部分。证明了一类特殊的相容合取BC演算公式构成一个无最大元的有界完全连续域（简称真BC域），并由此得到每个真BC域.更一般地，我们将合取后果关系表示为一致合取相继演算之间的态射，并建立一个与具有斯科特连续函数的真BC域等价的范畴。给出了真BC整环的纯句法形式的一个逻辑刻画。
Abstract We build a logical system named a conjunctive sequent calculus which is a conjunctive fragment of the classical propositional sequent calculus in the sense of proof theory. We prove that a special class of formulae of a consistent conjunctive sequent calculus forms a bounded complete continuous domain without greatest element (for short, a proper BC domain), and each proper BC domain can be obtained in this way. More generally, we present conjunctive consequence relations as morphisms between consistent conjunctive sequent calculi and build a category which is equivalent to that of proper BC domains with Scott-continuous functions. A logical characterization of purely syntactic form for proper BC domains is obtained.
登录
查看更多内容
DOI：
10.1007/bfb0012801
发表时间：
1982-07
期刊：
ACM Transactions on Database Systems (TODS)
影响因子：
--
作者：
D. Scott
通讯作者：
D. Scott
DOI：
10.1007/3-540-13346-1_5
发表时间：
1984-06
期刊：
--
影响因子：
--
作者：
G. Winskel;K. Larsen
通讯作者：
G. Winskel;K. Larsen
重新审视信息系统公理
影响因子：
1
作者：
Huang Mengqiao;Zhou Xiangnan;Li Qingguo
通讯作者：
Li Qingguo
DOI：
10.1093/acprof:oso/9780198568612.001.0001
发表时间：
2006
期刊：
--
影响因子：
--
作者：
S. Awodey
通讯作者：
S. Awodey
DOI：
10.1017/cbo9780511542725
发表时间：
2003-04
期刊：
--
影响因子：
--
作者：
G. Gierz;K. Hofmann;K. Keimel;J. Lawson;M. Mislove;D. Scott
通讯作者：
G. Gierz;K. Hofmann;K. Keimel;J. Lawson;M. Mislove;D. Scott