Open Access. Powered by Scholars. Published by Universities.®

Other Computer Engineering Commons

Open Access. Powered by Scholars. Published by Universities.®

Articles 1 - 3 of 3

Full-Text Articles in Other Computer Engineering

Tool Support For Reasoning In Display Calculi, Samuel Balco, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano Jan 2016

Tool Support For Reasoning In Display Calculi, Samuel Balco, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano

Engineering Faculty Articles and Research

We present a tool for reasoning in and about propositional sequent calculi. One aim is to support reasoning in calculi that contain a hundred rules or more, so that even relatively small pen and paper derivations become tedious and error prone. As an example, we implement the display calculus D.EAK of dynamic epistemic logic. Second, we provide embeddings of the calculus in the theorem prover Isabelle for formalising proofs about D.EAK. As a case study we show that the solution of the muddy children puzzle is derivable for any number of muddy children. Third, there is a set ...


Multi-Type Display Calculus For Dynamic Epistemic Logic, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano, Vlasta Sikimić Jan 2016

Multi-Type Display Calculus For Dynamic Epistemic Logic, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano, Vlasta Sikimić

Engineering Faculty Articles and Research

In the present paper, we introduce a multi-type display calculus for dynamic epistemic logic, which we refer to as Dynamic Calculus. The displayapproach is suitable to modularly chart the space of dynamic epistemic logics on weaker-than-classical propositional base. The presence of types endows the language of the Dynamic Calculus with additional expressivity, allows for a smooth proof-theoretic treatment, and paves the way towards a general methodology for the design of proof systems for the generality of dynamic logics, and certainly beyond dynamic epistemic logic. We prove that the Dynamic Calculus adequately captures Baltag-Moss-Solecki’s dynamic epistemic logic, and enjoys Belnap-style ...


Multi-Type Display Calculus For Propositional Dynamic Logic, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano Jan 2016

Multi-Type Display Calculus For Propositional Dynamic Logic, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano

Engineering Faculty Articles and Research

We introduce a multi-type display calculus for Propositional Dynamic Logic (PDL). This calculus is complete w.r.t. PDL, and enjoys Belnap-style cut-elimination and subformula property.