Labelled Non-Classical Logics

Front Cover
Springer Science & Business Media, Jan 31, 2000 - Computers - 291 pages
I am very happy to have this opportunity to introduce Luca Vigano's book on Labelled Non-Classical Logics. I put forward the methodology of labelled deductive systems to the participants of Logic Colloquium'90 (Labelled Deductive systems, a Position Paper, In J. Oikkonen and J. Vaananen, editors, Logic Colloquium '90, Volume 2 of Lecture Notes in Logic, pages 66-68, Springer, Berlin, 1993), in an attempt to bring labelling as a recognised and significant component of our logic culture. It was a response to earlier isolated uses of labels by various distinguished authors, as a means to achieve local proof theoretic goals. Labelling was used in many different areas such as resource labelling in relevance logics, prefix tableaux in modal logics, annotated logic programs in logic programming, proof tracing in truth maintenance systems, and various side annotations in higher-order proof theory, arithmetic and analysis. This widespread local use of labels was an indication of an underlying logical pattern, namely the simultaneous side-by-side manipulation of several kinds of logical information. It was clear that there was a need to establish the labelled deductive systems methodology. Modal logic is one major area where labelling can be developed quickly and sys tematically with a view of demonstrating its power and significant advantage. In modal logic the labels can play a double role.
 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

INTRODUCTION
1
12 CONTRIBUTION
3
13 MAIN RESULTS
12
14 SYNOPSIS
13
LABELLED NATURAL DEDUCTION SYSTEMS FOR PROPOSITIONAL MODAL LOGICS
17
21 A MODULAR PRESENTATION OF PROPOSITIONAL MODAL LOGICS
18
22 SOUNDNESS AND COMPLETENESS
29
23 NORMALIZATION AND ITS CONSEQUENCES
37
63 EQUIVALENCE OF LABELLED NATURAL DEDUCTION AND SEQUENT SYSTEMS
149
DISCUSSION
157
INTRODUCTION AND PRELIMINARIES
167
82 PRELIMINARY RESULTS
170
SUBSTRUCTURAL ANALYSIS OF SK
187
92 SK AND SSK
195
SUBSTRUCTURAL ANALYSIS OF ST
201
102 ST AND SST
219

LABELLED NATURAL DEDUCTION SYSTEMS FOR PROPOSITIONAL NONCLASSICAL LOGICS
53
31 MODULAR PRESENTATIONS OF PROPOSITIONAL NONCLASSICAL LOGICS
54
32 SOUNDNESS AND COMPLETENESS
71
33 NORMALIZATION AND ITS CONSEQUENCES
81
LABELLED NATURAL DEDUCTION SYSTEMS FOR QUANTIFIED MODAL LOGICS
91
41 A MODULAR PRESENTATION OF QUANTIFIED MODAL LOGICS
93
42 SOUNDNESS AND COMPLETENESS
100
43 NORMALIZATION AND ITS CONSEQUENCES
107
ENCODING LABELLED NONCLASSICAL LOGICS IN ISABELLE
115
52 ENCODING PROPOSITIONAL NONCLASSICAL LOGICS
126
53 ENCODING QUANTIFIED MODAL LOGICS
131
LABELLED SEQUENT SYSTEMS FOR NONCLASSICAL LOGICS
137
61 LABELLED SEQUENT SYSTEMS FOR PROPOSITIONAL MODAL LOGICS
138
62 LABELLED SEQUENT SYSTEMS FOR NONCLASSICAL LOGICS
147
SUBSTRUCTURAL ANALYSIS OF SK4 AND SS4
223
111 INFINITE CHAINS INFINITE BRANCHES AND PERIODICITY
225
112 BOUNDING CONTRACTION IN SK4 AND SS4
230
113 SK4 AND SSK4
238
114 SS4 AND SSS4
245
COMPLEXITY OF PROOF SEARCH IN K T K4 AND S4
247
122 COMPLEXITY OF PROOF SEARCH IN K
248
123 COMPLEXITY OF PROOF SEARCH IN T
250
124 COMPLEXITY OF PROOF SEARCH IN K4 AND S4
251
DISCUSSION
253
CONCLUSIONS AND FURTHER RESEARCH
263
References
267
Index
283
Copyright

Other editions - View all

Common terms and phrases

About the author (2000)

Luca Vigaṇ is an assistant professor at the Institute for Computer Science of the University of Freiburg (Germany). His research focuses on the theory and applications of non-classical logics, of proof development systems, of logical frameworks, and of logics for security.

Bibliographic information