Skip to content

Research at St Andrews

Algebra, proof theory and applications for an intuitionistic logic of propositions, actions and adjoint modal operators

Research output: Research - peer-reviewArticle

DOI

Author(s)

Roy Dyckhoff, Mehrnoosh Sadrzadeh, Julien Truffaut

School/Research organisations

Abstract

We develop a cut-free nested sequent calculus as basis for a proof search procedure for an intuitionistic 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). The logic has agent-indexed adjoint pairs of epistemic modalities: the left adjoints encode agents’ uncertainties and the right adjoints encode their beliefs. The rules for the “update” modality encode learning as a result of discarding uncertainty. We prove admissibility of Cut, and hence the soundness and completeness of the logic with respect to an algebraic semantics. We interpret the logic on epistemic scenarios that consist of honest and dishonest communication actions, add assumption rules to encode them, and prove that the
calculus with the assumption rules still has the admissibility results. We apply the calculus to encode (and allow reasoning about) the classic epistemic puzzles of
dirty children (aka “muddy children”) and drinking logicians and some versions with dishonesty or noise; we also give an application where the actions are movements of a robot rather than announcements.

Close

Details

Original languageEnglish
Article number34
Number of pages38
JournalACM Transactions on Computational Logic
Volume14
Issue number4
DOIs
StatePublished - Nov 2013

    Research areas

  • Proof theory, Cut admissibility, Algebra, Adjoint modalities, actions, Adjoint modal operators

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Analyticity, balance and non-admissibility of Cut in Stoic Logic

    Bobzien, S. & Dyckhoff, R. 20 Apr 2018 In : Studia Logica. First Online, 23 p.

    Research output: Research - peer-reviewArticle

  2. Intuitionistic decision procedures since Gentzen

    Dyckhoff, R. 5 May 2016 Advances in Proof Theory. Kahle, R., Strahm, T. & Studer, T. (eds.). Birkhäuser Basel, p. 245-267 (Progress in Computer Science and Applied Logic; vol. 28)

    Research output: Research - peer-reviewChapter (peer-reviewed)

  3. POSIX lexing with derivatives of regular expressions (proof pearl)

    Ausaf, F., Dyckhoff, R. & Urban, C. 2016 Interactive Theorem Proving: 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings. Blanchette, J. C. & Merz, S. (eds.). Springer, p. 69-86 18 p. (Lecture Notes in Computer Science; vol. 9807)

    Research output: ResearchConference contribution

  4. Some remarks on proof-theoretic semantics

    Dyckhoff, R. 2016 Advances in Proof-Theoretic Semantics. Piecha, T. & Schroeder-Heister, P. (eds.). Springer, p. 79-93 15 p. (Trends in Logic; vol. 43)

    Research output: Research - peer-reviewChapter (peer-reviewed)

Related by journal

  1. Foundational certified code in the Twelf metalogical framework

    Crary, K. & Sarkar, S. 2008 In : ACM Transactions on Computational Logic. 9, 3, 26 p., ARTN 16

    Research output: Research - peer-reviewArticle

ID: 110579706