Name
Title | ||
|---|---|---|
Algebra, Proof Theory and Applications for a Logic of Propositions, Actions and Adjoint Modal Operators |
Abstract | ||
|---|---|---|
We develop a cut-free (and hence analytic) nested sequent calculus for a modal logic of actions and propositions. The actions act on propositions via a dynamic modality (the weakest precondition of program logics), whose left adjoint we refer to as 'update' (the strongest postcondition). Both logics are positive and have adjoint pairs of epistemic modalities: the left adjoints express agents@? uncertainties and the right adjoints express their beliefs. The rules for 'update' encode learning as a result of discarding uncertainty. We prove admissibility of Cut, and hence the completeness of the logic w.r.t. an algebraic semantics. We interpret the logic on epistemic scenarios with honest and dishonest communication actions, add assumption rules to encode them and prove that the extended calculus still has the admissibility results. We apply the calculus to encode and solve the classic epistemic puzzle of muddy children and a modern version of it with dishonest agents. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1016/j.entcs.2012.08.011 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
extended calculus,epistemic modality,modal logic,adjoint modal operators,nested sequent calculus,classic epistemic puzzle,program logic,epistemic scenario,admissibility result,logic w,proof theory,adjoint pair,algebra | Predicate transformer semantics,Discrete mathematics,Algebra,Computer science,Sequent calculus,Proof theory,Modal operator,Modal logic,Postcondition,Completeness (statistics),Algebraic semantics | Journal |
Volume | ISSN | Citations |
286, | 1571-0661 | 1 |
PageRank | References | Authors |
0.36 | 10 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Roy Dyckhoff | 1 | 452 | 49.09 |
| Mehrnoosh Sadrzadeh | 2 | 784 | 62.69 |
| Julien Truffaut | 3 | 4 | 0.79 |