Effective Method to Obtain Terminating Proof-Search in Transitive Multimodal Logics ; Efektyvus metodas baigtinei išvedimo paieškai tranzityviose multimodalinėse logikose gauti

Sujets

• Mathematics
• Modal logic
• Termination

Informations

• Publié par: vilnius_university
• Publié le: 01 janvier 2011
• Nombre de lectures: 13
• Langue: English

Extrait

VILNIUS UNIVERSITY
Julius Andrikonis
Effective Method to Obtain Terminating
Proof-Search in Transitive Multimodal Logics
Doctoral dissertation
Physical sciences, Mathematics (01 P)
Vilnius, 2011The dissertation was prepared in 2006–2011 at Institute of Mathematics
and Informatics, Vilnius University, Lithuania.
Research supervisor:
Assoc. Prof. Habil. Dr. Regimantas Pliuškevičius (Vilnius University,
physical sciences, mathematics — 01 P).VILNIAUS UNIVERSITETAS
Julius Andrikonis
Efektyvus metodas baigtinei išvedimo paieškai
tranzityviose multimodalinėse logikose gauti
Daktaro disertacija
Fiziniai mokslai, Matematika (01 P)
Vilnius, 2011Disertacija rengta 2006–2011 metais Vilniaus universiteto Matematikos
ir informatikos institute.
Mokslinis vadovas:
doc. habil. dr. Regimantas Pliuškevičius (Vilniaus universitetas, fiziniai
mokslai, matematika — 01 P).Abstract
The knowledge of agents is usually modelled using logic S5. However in
some cases it is preferable to use other modal logics, for example S4 or even
its multimodal variant S4 . It also can be noted, that S5 can be triviallyn
embedded into S4 ([14]) and the satisfiability problem for S4 is PSPACE-n
complete ([35]). Although multimodal epistemic logics are capable of mod-
elling knowledge of many different agents, they do not include interaction
between them. In this dissertation one particular form of in is
chosen: one of the agents is called the central agent, because it knows ev-
erything that is known to other agents. This interaction is essentially the
same as distributed knowledge.
The main aim of this thesis is to present a sequent calculus for multi-
modal logic S4 with central agent axiom in which every derivation searchn
terminates. To achieve this task, basic sequent calculus is derived from the
respective Hilbert-type calculus and the cut-elimination theorem is proved.
Next the obtained calculus is modified to ensure the termination of deriva-
tion search. This is done using different kind of labels: positive and negative
indexes of the modality, stars of the negatively indexed modality, marks of
the positively indexed modality and formula numbers. These labels are
used to restrict the applications of the rules, which causes loops in deriva-
tion search trees.
Moreover, the research allowed to extend the results to other logics, there-
fore terminating calculi for multimodal epistemic logics K , T and K4n n n
with central agent axiom are also presented. Although termination of proof
search in the sequent calculi for K and T with central agent axiom is ob-n n
tained with only little or no effort, the transitivity axiomF⊃F ofl l l
logics K4 and S4 with central agent axiom causes much more difficulties.n n
To solve these problems, the new terminating calculi for monomodal logics
K4 and S4 are derived and also presented in this thesis.
Needless to say, that this thesis also proves the soundness and complete-
1ness of every newly introduced calculus. It also shows, that every derivation
search in each of the terminating calculi is finite.Acknowledgements
Dedication:
I dedicate this work to my father Juozapas Andrikonis, who
once wished to complete doctoral studies, however chose to sacrifice
his own aspirations in order to devote more time for raising me and
my siblings.
I wish to express my gratitude to all the people who helped me during this
work. I cannot thank enough to my supervisor Assoc. Prof. Habil. Dr. Regi-
mantas Pliuškevičius for his knowledge and experience he kindly shared with
me. I am pleased to thank to the scientists of the Mathematical Logic Sec-
tor of SED in Vilnius University Institute of Mathematics and Informatics
and to my colleagues in The Faculty of Mathematics and Informatics of Vil-
nius University for valuable discussions and suggestions about improving my
work. My special gratitude goes to Dr. Romas Alonderis, the reviewer of
the dissertation, for detailed comments and consultations. I am grateful to
Doc. Dr. Stanislovas Norgėla for constructive remarks and to Dr. Adomas
Birštunas for sharing his recent experience about defending the doctoral
thesis.
I am indebted to my family for making this research possible, especially to
my parents Juozapas Andrikonis and Virginija Andrikonienė for enormous
moral and financial support. I am truly grateful to my wife Viktorija and
daughter Ieva for understanding and patience, which allowed me to dedicate
time to the research.
3Contents
Abstract 1
Acknowledgements 3
Table of Contents 6
Introduction 7
Research Area and Problem relevance . . . . . . . . . . . . . . . . 7h Objectives . . . . . . . . . . . . . . . . . . . . . . . . . 8
Aim of the Work and Work Tasks . . . . . . . . . . . . . . . . . . 8
Methods . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
Scientific Novelty . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
Defending Statements . . . . . . . . . . . . . . . . . . . . . . . . 11
Approval of Research Results . . . . . . . . . . . . . . . . . . . . 11
Publications of the Author . . . . . . . . . . . . . . . . . . . . . . 12
Outline of the Dissertation . . . . . . . . . . . . . . . . . . . . . . 12
1 Initial Calculi 14
1.1 Classical Propositional Calculi . . . . . . . . . . . . . . . . . 14
1.2 Modal Calculi . . . . . . . . . . . . . . . . . . . . . . . . . . 20
1.3 Multimodal Calculi . . . . . . . . . . . . . . . . . . . . . . . 24
1.4 Some Properties of the Calculi . . . . . . . . . . . . . . . . . 27
2 Basic Calculi for Multimodal Logics with Interaction 40
2.1 Central Agent Axiom . . . . . . . . . . . . . . . . . . . . . . 40
2.2 Hilbert-type Calculi . . . . . . . . . . . . . . . . . . . . . . . 43
2.3 Gentzen-type Calculi with Cut . . . . . . . . . . . . . . . . . 44
2.4 Gentzen-type Calculi without Cut . . . . . . . . . . . . . . . 59
53 Terminating Calculi for Multimodal Logics with Interaction 74
c3.1 Logic K . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74n
c
3.2 Logic T . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75n
3.3 Logic S4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
c
3.4 Logic S4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84n
3.4.1 The Calculus . . . . . . . . . . . . . . . . . . . . . . 84
3.4.2 Finiteness of Derivation Search in the Calculus . . . . 90
3.4.3 Soundness and Completeness of the . . . . . 97
c
3.5 Logics K4 and K4 . . . . . . . . . . . . . . . . . . . . . . . 107n
Conclusions 110
Bibliography 111
A Proof of Lemma 2.3.6 116
c c c c
A.1 Formulas Derivable in HK , HK4 , HT and HS4 . . . . . . 116n n n n
c c
A.2 Formula Derivable in HK4 and HS4 . . . . . . . . . . . . . 118n n