Hostname: page-component-78c5997874-fbnjt Total loading time: 0 Render date: 2024-11-07T20:15:09.324Z 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, China School 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: [email protected]
Get access Rights & Permissions [Opens in a new window]

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.

Keywords

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

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

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