Commit 765383bd authored by Gerwin Klein's avatar Gerwin Klein
Browse files

regen website

parent 1a8521c8ed48
......@@ -2,7 +2,7 @@
<html lang="en">
<head>
<meta charset="utf-8">
<title>Epistemic Logic - Archive of Formal Proofs
<title>Epistemic Logic: Completeness of Modal Logics - Archive of Formal Proofs
</title>
<link rel="stylesheet" type="text/css" href="../front.css">
<link rel="icon" href="../images/favicon.ico" type="image/icon">
......@@ -76,7 +76,15 @@ MathJax = {
<p>&nbsp;</p>
<h1> <font class="first">E</font>pistemic
<font class="first">L</font>ogic
<font class="first">L</font>ogic:
<font class="first">C</font>ompleteness
of
<font class="first">M</font>odal
<font class="first">L</font>ogics
</h1>
<p>&nbsp;</p>
......@@ -85,7 +93,7 @@ MathJax = {
<tbody>
<tr>
<td class="datahead" width="20%">Title:</td>
<td class="data" width="80%">Epistemic Logic</td>
<td class="data" width="80%">Epistemic Logic: Completeness of Modal Logics</td>
</tr>
<tr>
......@@ -111,16 +119,23 @@ 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" by Fagin, Halpern, Moses and
Vardi (MIT Press 1995).</td>
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).</td>
</tr>
<tr>
<td class="datahead" valign="top">Change history:</td>
<td class="abstract">[2020-04-15]: Added completeness of modal logics T, KB, K4, S4 and S5.</td>
</tr>
<tr>
<td class="datahead" valign="top">BibTeX:</td>
<td class="formatted">
<pre>@article{Epistemic_Logic-AFP,
author = {Asta Halkjær From},
title = {Epistemic Logic},
title = {Epistemic Logic: Completeness of Modal Logics},
journal = {Archive of Formal Proofs},
month = oct,
year = 2018,
......
......@@ -129,9 +129,8 @@ while guaranteeing certain correctness and security properties for all
well-typed programs. We formalize &lambda;&bull; and prove its
correctness and security properties. With Isabelle's help, we
uncover and repair several mistakes in the informal proofs and lemma
statements. Our findings are summarized in a <a
href="http://people.inf.ethz.ch/trayteld/papers/lambdaauth/lambdaauth.pdf">paper
draft</a>.</td>
statements. Our findings are summarized in an <a
href="https://doi.org/10.4230/LIPIcs.ITP.2019.10">ITP'19 paper</a>.</td>
</tr>
......
......@@ -1411,7 +1411,7 @@ of a scientific journal, is indexed by <a href="http://dblp.uni-trier.de/db/jour
</tr>
<tr>
<td class="entry">
2018-10-29: <a href="entries/Epistemic_Logic.html">Epistemic Logic</a>
2018-10-29: <a href="entries/Epistemic_Logic.html">Epistemic Logic: Completeness of Modal Logics</a>
<br>
Author:
<a href="https://people.compute.dtu.dk/ahfrom/">Asta Halkjær From</a>
......
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment