Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
isa-afp
afp-devel
Commits
77def7de7e09
Commit
9659136e
authored
Apr 15, 2021
by
Asta H. From
Browse files
Add completeness of modal logics T, KB, K4, S4 and S5
parent
8f1f310afd72
Changes
4
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
1045 additions
and
249 deletions
+1045
-249
metadata/metadata
metadata/metadata
+7
-1
thys/Epistemic_Logic/Epistemic_Logic.thy
thys/Epistemic_Logic/Epistemic_Logic.thy
+1015
-244
thys/Epistemic_Logic/document/root.bib
thys/Epistemic_Logic/document/root.bib
+17
-1
thys/Epistemic_Logic/document/root.tex
thys/Epistemic_Logic/document/root.tex
+6
-3
No files found.
metadata/metadata
View file @
77def7de
...
...
@@ -3988,7 +3988,7 @@ extra-history =
notify = berghofe@in.tum.de
[Epistemic_Logic]
title = Epistemic Logic
title = Epistemic Logic
: Completeness of Modal Logics
author = Asta Halkjær From <https://people.compute.dtu.dk/ahfrom/>
topic = Logic/General logic/Logics of knowledge and belief
date = 2018-10-29
...
...
@@ -3999,6 +3999,12 @@ abstract =
system K. The completeness proof is based on the textbook
"Reasoning About Knowledge" by Fagin, Halpern, Moses and
Vardi (MIT Press 1995).
The extensions of system K (T, KB, K4, S4, S5) and their completeness proofs
are based on the textbook "Modal Logic" by Blackburn, de Rijke and Venema
(Cambridge University Press 2001).
extra-history =
Change history:
[2020-04-15]: Added completeness of modal logics T, KB, K4, S4 and S5.
[SequentInvertibility]
title = Invertibility in Sequent Calculi
...
...
thys/Epistemic_Logic/Epistemic_Logic.thy
View file @
77def7de
This diff is collapsed.
Click to expand it.
thys/Epistemic_Logic/document/root.bib
View file @
77def7de
...
...
@@ -5,4 +5,20 @@
year
=
{1995}
,
isbn
=
{0262061627}
,
author
=
{Fagin, R. and Halpern, J.Y. and Moses, Y. and Vardi, M.Y.}
}
\ No newline at end of file
}
@book
{
blackburn2001
,
author
=
{Patrick Blackburn and
Maarten de Rijke and
Yde Venema}
,
title
=
{Modal Logic}
,
series
=
{Cambridge Tracts in Theoretical Computer Science}
,
volume
=
{53}
,
publisher
=
{Cambridge University Press}
,
year
=
{2001}
,
url
=
{https://doi.org/10.1017/CBO9781107050884}
,
doi
=
{10.1017/CBO9781107050884}
,
isbn
=
{978-1-10705088-4}
}
thys/Epistemic_Logic/document/root.tex
View file @
77def7de
\documentclass
[11pt,a4paper]
{
article
}
\usepackage
[
T1]
{
fon
tenc
}
\usepackage
[
utf8]
{
inpu
tenc
}
\usepackage
{
isabelle,isabellesym
}
\usepackage
{
amssymb
}
...
...
@@ -16,15 +16,18 @@
\begin{document}
\title
{
Epistemic Logic
}
\title
{
Epistemic Logic
: Completeness of Modal Logics
}
\author
{
Asta Halkjær From
}
\maketitle
\begin{abstract}
This work is a formalization of epistemic logic with countably many agents.
It includes proofs of soundness and completeness for the axiom system K.
The completeness proof is based on the textbook
``
Reasoning About Knowledge
''
The completeness proof is based on the textbook
"
Reasoning About Knowledge
"
by Fagin, Halpern, Moses and Vardi (MIT Press 1995)~
\cite
{
fagin1995
}
.
The extensions of system K (T, KB, K4, S4, S5) and their completeness proofs
are based on the textbook "Modal Logic" by Blackburn, de Rijke and Venema
(Cambridge University Press 2001)~
\cite
{
blackburn2001
}
.
\end{abstract}
\tableofcontents
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment