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: Contribution to journalArticle

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. 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: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

  2. 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: Chapter in Book/Report/Conference proceedingConference contribution

  3. 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: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

  4. Geometrisation of first-order logic

    Dyckhoff, R. & Negri, S. Jun 2015 In : Bulletin of Symbolic Logic. 21, 2, p. 123–163 41 p.

    Research output: Contribution to journalArticle

  5. Cut-elimination, substitution and normalisation

    Dyckhoff, R. 2015 Dag Prawitz on Proofs and Meaning. Wansing, H. (ed.). Springer, p. 163-187 (Outstanding Contributions to Logic; vol. 7)

    Research output: Chapter in Book/Report/Conference proceedingChapter (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: Contribution to journalArticle

ID: 110579706