Showing 1–5 of 5 results for author: Ciabattoni, A

Internal and External Calculi: Ordering the Jungle without Being Lost in Translations

Authors: Tim S. Lyon, Agata Ciabattoni, Didier Galmiche, Marianna Girlando, Dominique Larchey-Wendling, Daniel Méry, Nicola Olivetti, Revantha Ramanayake

Abstract: This paper gives a broad account of the various sequent-based proof formalisms in the proof-theoretic literature. We consider formalisms for various modal and tense logics, intuitionistic logic, conditional logics, and bunched logics. After providing an overview of the logics and proof formalisms under consideration, we show how these sequent-based formalisms can be placed in a hierarchy in terms… ▽ More This paper gives a broad account of the various sequent-based proof formalisms in the proof-theoretic literature. We consider formalisms for various modal and tense logics, intuitionistic logic, conditional logics, and bunched logics. After providing an overview of the logics and proof formalisms under consideration, we show how these sequent-based formalisms can be placed in a hierarchy in terms of the underlying data structure of the sequents. We then discuss how this hierarchy can be traversed using translations. Translating proofs up this hierarchy is found to be relatively straightforward while translating proofs down the hierarchy is substantially more difficult. Finally, we inspect the prevalent distinction in structural proof theory between 'internal calculi' and 'external calculi.' We discuss the ambiguities involved in the informal definitions of these categories, and we critically assess the properties that (calculi from) these classes are purported to possess. △ Less

Submitted 7 May, 2025; v1 submitted 6 December, 2023; originally announced December 2023.

Comments: Published in the Bulletin of the Section of Logic

Display to Labeled Proofs and Back Again for Tense Logics

Authors: Agata Ciabattoni, Tim S. Lyon, Revantha Ramanayake, Alwen Tiu

Abstract: We introduce translations between display calculus proofs and labeled calculus proofs in the context of tense logics. First, we show that every derivation in the display calculus for the minimal tense logic Kt extended with general path axioms can be effectively transformed into a derivation in the corresponding labeled calculus. Concerning the converse translation, we show that for Kt extended wi… ▽ More We introduce translations between display calculus proofs and labeled calculus proofs in the context of tense logics. First, we show that every derivation in the display calculus for the minimal tense logic Kt extended with general path axioms can be effectively transformed into a derivation in the corresponding labeled calculus. Concerning the converse translation, we show that for Kt extended with path axioms, every derivation in the corresponding labeled calculus can be put into a special form that is translatable to a derivation in the associated display calculus. A key insight in this converse translation is a canonical representation of display sequents as labeled polytrees. Labeled polytrees, which represent equivalence classes of display sequents modulo display postulates, also shed light on related correspondence results for tense logics. △ Less

Submitted 6 May, 2021; v1 submitted 6 November, 2019; originally announced November 2019.

Hypersequents and Systems of Rules: Embeddings and Applications

Authors: Agata Ciabattoni, Francesco A. Genco

Abstract: We define a bi-directional embedding between hypersequent calculi and a subclass of systems of rules (2-systems). In addition to showing that the two proof frameworks have the same expressive power, the embedding allows for the recovery of the benefits of locality for 2-systems, analyticity results for a large class of such systems, and a rewriting of hypersequent rules as natural deduction rules. We define a bi-directional embedding between hypersequent calculi and a subclass of systems of rules (2-systems). In addition to showing that the two proof frameworks have the same expressive power, the embedding allows for the recovery of the benefits of locality for 2-systems, analyticity results for a large class of such systems, and a rewriting of hypersequent rules as natural deduction rules. △ Less

Submitted 13 May, 2018; originally announced May 2018.

Comments: 32 pages, the final publication is available at ACM DL via https://dl.acm.org/citation.cfm?id=3180075

Journal ref: ACM Transactions on Computational Logic (TOCL). Volume 19, Issue 2, Article No. 11. 2018

Disjunctive Axioms and Concurrent $λ$-Calculi: a Curry-Howard Approach

Authors: F. Aschieri, A. Ciabattoni, F. A. Genco

Abstract: We add to intuitionistic logic infinitely many classical disjunctive tautologies and use the Curry--Howard correspondence to obtain typed concurrent $λ$-calculi; each of them features a specific communication mechanism, including broadcasting and cyclic message-exchange, and enhanced expressive power with respect to the $λ$-calculus. Moreover they all implement forms of code mobility. Our results… ▽ More We add to intuitionistic logic infinitely many classical disjunctive tautologies and use the Curry--Howard correspondence to obtain typed concurrent $λ$-calculi; each of them features a specific communication mechanism, including broadcasting and cyclic message-exchange, and enhanced expressive power with respect to the $λ$-calculus. Moreover they all implement forms of code mobility. Our results provide a first concurrent computational interpretation for many propositional intermediate logics, classical logic included. △ Less

Submitted 13 February, 2018; v1 submitted 3 February, 2018; originally announced February 2018.

Quantified propositional Goedel logics

Authors: Matthias Baaz, Agata Ciabattoni, Richard Zach

Abstract: It is shown that G-up, the quantified propositional Goedel-Dummett logic based on the truth-values set V-up = {1 - 1/n : n >= 1} u {1}, is decidable. This result is obtained by reduction to Buechi's theory S1S. An alternative proof based on elimination of quantifiers is also given, which yields both an axiomatization and a characterization of G-up as the intersection of all finite-valued quantif… ▽ More It is shown that G-up, the quantified propositional Goedel-Dummett logic based on the truth-values set V-up = {1 - 1/n : n >= 1} u {1}, is decidable. This result is obtained by reduction to Buechi's theory S1S. An alternative proof based on elimination of quantifiers is also given, which yields both an axiomatization and a characterization of G-up as the intersection of all finite-valued quantified propositional Goedel logics. △ Less

Submitted 3 October, 2000; v1 submitted 17 June, 2000; originally announced June 2000.

Comments: v.2: 17 pages, revised published version (v.1: 15 pages)

MSC Class: 03B50; 03B55

Journal ref: Michel Parigot, Andrei Voronkov (Eds.): Logic for Programming and Automated Reasoning. 7th International Conference, LPAR 2000, Reunion Island, France, November 11-12, 2000. Lecture Notes in Computer Science, Vol. 1955, Springer, 2000. pp. 240-256