Hostname: page-component-7b7567c8c-tnzcf Total loading time: 0 Render date: 2026-11-15T08:09:05.253Z Has data issue: false hasContentIssue false
  • English
  • Français

A representation of proper BC domains based on conjunctive sequent calculi

Published online by Cambridge University Press:  16 October 2019

Longchun Wang and
Qingguo Li
Longchun Wang
Affiliation:
College of Mathematics and Econometrics, Hunan University, Changsha, 410082, ChinaSchool of Mathematical Sciences, Qufu Normal University, Qufu, 273165, China
Qingguo Li*
Affiliation:
College of Mathematics and Econometrics, Hunan University, Changsha, 410082, China
*
*Corresponding author. Email: liqingguoli@aliyun.com
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

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.

Keywords

Conjunctive sequent calculusproper BC domaincategorical equivalence

Information

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 30 , Issue 1 , January 2020, pp. 1 - 13
Copyright
© Cambridge University Press 2019 

Footnotes

†

This research Supported by the National Natural Science Foundation of China(11771134).

References

Abramsky, S. (1991). Domain theory in logical form. Annals of Pure and Applied Logic 51 1–77.CrossRefGoogle Scholar
Awodey, S. (2006). Category Theory, Oxford Logic Guides, vol. 52. New York, Oxford University Press.CrossRefGoogle Scholar
Chen, Y. and Jung, A. (2006). A logical approach to stable domains. Theoretical Computer Science 368 124–148.CrossRefGoogle Scholar
Davey, B. A. and Priestly, H. A. (2002). Introduction to Lattices and Order. Cambridge, Cambridge University Press.CrossRefGoogle Scholar
Gallier, J. H. (2015). Logic for Computer Science: Foundations of Automatic Theorem Proving. New York, Courier Dover Publications.Google Scholar
Gierz, G., Hofmann, K. H., Keimel, K., Lawson, J. D., Mislove, M. and Scott, D. S. (2003). Continuous Lattices and Domains, Encyclopedia of Mathematics and its Applications, vol. 93. Cambridge, Cambridge University Press.CrossRefGoogle Scholar
Goubault-Larrecq, J. (2013). Non-Hausdorff Topology and Domain Theory, New Mathematical Monographs, vol. 22. Cambridge, Cambridge University Press.CrossRefGoogle Scholar
Hitzler, P., Krötzsch, M., and Zhang, G. (2006). A categorical view on algebraic lattices in formal concept analysis. Fundamenta Informaticae 74 1–29.Google Scholar
Hoofman, R. (1993). Continuous information systems. Information and Computation 105 42–71.CrossRefGoogle Scholar
Huang, M., Zhou, X., and Li, Q. (2015). Re-visiting axioms of information systems. Information and Compution 247 130–140.CrossRefGoogle Scholar
Jung, A., Kegelmann, M., and Moshier, M. A. (1999). Multi lingual sequent calculus and coherent spaces. Fundamenta Informaticae 37 369–412.CrossRefGoogle Scholar
Jung, A. (2013). Continuous domain theory in logical form. In: Coecke, B., Ong, L., and Panangaden, P. (eds.) Computation, Logic, Games, and Quantum Foundations, Lecture Notes in Computer Science, vol. 7860, Berlin, Heidelberg, Springer, 166–177.Google Scholar
Larsen, K. G. and Winskel, G. (1984). Using information systems to solve recursive domain equations effectively. In: Kahn, G., MacQueen, D. B., and Plotkin, G. (eds.) Semantics of Data Types, Lecture Notes in Computer Science, vol. 173, Berlin, Heidelberg, Springer, 109–130.CrossRefGoogle Scholar
Scott, D. S. (1982). Domains for denotational semantics. In: Nielson, M. and Schmidt, E. M. (eds.) International Colloquium on Automata, Languages and Programs, Lecture Notes in Computer Science, vol. 140, Berlin, Heidelberg, Springer, 577–613.CrossRefGoogle Scholar
Spreen, D., Xu, L., and Mao, X. (2008). Information systems revisited: The general continuous case. Theoretical Computer Science 405 176–187.CrossRefGoogle Scholar
Vickers, S. J. (1993). Information systems for continuous posets. Theoretical Computer Science 114, 201–229.CrossRefGoogle Scholar
Wang, G. and Zhou, H. (2009). Introduction to Mathematical Logic and Resolution Principle, Mathematicas Monograph Series, vol. 13. Beijing, Science Press.Google Scholar
Wu, M., Guo, L., and Li, Q. (2016). A representation of L-domains by information system. Theoretical Computer Science 612 126–136.CrossRefGoogle Scholar
Zhang, G. (1992). Disjunctive systems and L-domains. In: Kuich, W. (ed.) International Conference on Automata, Languages and Programming, Vienna 1992, Lecture Notes in Computer Science, vol. 623, Berlin, Heidelberg, Springer, 284–295.Google Scholar