A Sequent Calculus for 3-Dimensional Space

  • Norihiro Kamide
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6404)


A central issue for spatial reasoning in practice is to formalize reasoning about 3-dimensional space. In this paper, a spatial logic called 3-dimensional spatial logic (3SL), which can appropriately represent the 3-Cartesian product ω 3 of the set ω of natural numbers, is introduced as a Gentzen-type sequent calculus. 3SL is an extension and generalization of the linear-time temporal logic LTL in which the time domain is ω. The completeness and cut-elimination theorems for 3SL are proved.


Propositional Variable Completeness Theorem Spatial Reasoning Classical Propositional Logic Satisfaction Relation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Formal Models and Semantics (B), pp. 995–1072. Elsevier, MIT Press (1990)Google Scholar
  2. 2.
    Kamide, N.: Embedding linear-time temporal logic into infinitary logic: Application to cut-elimination for multi-agent infinitary epistemic linear-time temporal logic. In: Fisher, M., Sadri, F., Thielscher, M. (eds.) CLIMA IX. LNCS (LNAI), vol. 5405, pp. 57–76. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  3. 3.
    Kawai, H.: Sequential calculus for a first order infinitary temporal logic. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 33, 423–432 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46–57 (1977)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Norihiro Kamide
    • 1
  1. 1.Waseda Institute for Advanced StudyWaseda UniversityTokyoJapan

Personalised recommendations