A first-order dynamic non-commutative logic, which has no structural rules and has some program operators, is introduced as a Gentzen-type sequent calculus. Decidability, cut-elimination and completeness theorems are shown for DN or its fragments. DN is intended to represent not only program-based, resource-sensitive, ordered, sequence-based, but also hierarchical reasoning.
Keywords Completeness  Cut-elimination  Decidability  Dynamic logic  Non-commutative logic  Sequent calculus
Categories (categorize this paper)
Reprint years 2009, 2010
DOI 10.1007/s10849-009-9101-1
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 50,447
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Dynamic Logic.Lenore D. Zuck & David Harel - 1989 - Journal of Symbolic Logic 54 (4):1480.
The Mathematics of Sentence Structure.Joachim Lambek - 1968 - Journal of Symbolic Logic 33 (4):627-628.
Non-Commutative Intuitionistic Linear Logic.V. Michele Abrusci - 1990 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 36 (4):297-318.
Predicate Logics Without the Structure Rules.Yuichi Komori - 1986 - Studia Logica 45 (4):393 - 404.

View all 9 references / Add more references

Citations of this work BETA

Bunched Sequential Information.Norihiro Kamide - 2016 - Journal of Applied Logic 15:150-170.

Add more citations

Similar books and articles


Added to PP index

Total views
39 ( #241,720 of 2,326,393 )

Recent downloads (6 months)
4 ( #212,154 of 2,326,393 )

How can I increase my downloads?


My notes