full screen background image


PhD Thesis

    Paolo Baldi ( Standard completeness: proof-theoretic and algebraic methods ), defended August 2015
    Lara Spendier (Tools for the Investigation of Non-classical Logics ), defended June 2015


  1. A. Ciabattoni, T. Lyon, and R. Ramanayake. From Display to Labelled Proofs for Tense Logics. Proceedings of LFCS 2018.
  2. 2017

    1. F. Aschieri, A. Ciabattoni, F. Genco. Goedel Logic: From Natural Deduction to Parallel Computation. Proceedings of LICS 2017
    2. A. Ciabattoni and F. Genco. Hypersequents and Systems of Rules: Embeddings and Applications. ACM Transaction on Computational Logic. To appear.
    3. A. Ciabattoni, N. Galatos and K. Terui. Algebraic proof theory: hypersequents and hypercompletions. Annals of Pure and Applied Logic. 168(3): 693-737, 2017.
    4. A. Ciabattoni, B, Lellmann, C. Olarte and E. Pimentel. From cut-free calculi to automated deduction: the case of bounded contraction. Accepted for publication in ENTCS
    5. A. Ciabattoni and R. Ramanayake. Bunched Hypersequent Calculi for Distributive Substructural Logics. Proceedings of LPAR-21
    6. P. Baldi, A. Ciabattoni and F. Giulisano. Standard completeness for extensions of IMTL. Proceedings of FUZZ-IEEE 2017: International Conference on Fuzzy Systems


    1. A. Ciabattoni and R. Ramanayake. Power and limits of structural display rules. ACM Trans. Comput. Log. 17(3): 17 .
    2. M. Baaz and A. Ciabattoni. Proof theory of witnessed Goedel logic: a negative result. Journal of Logic and Computation 26(1): 51-64 (2016)
    3. R. Ramanayake Non-commutative classical arithmetical sequent calculi are intuitionistic. Journal of the IGPL , 24(3), pp 441-452, 2016
    4. A. Ciabattoni, F. A. Genco, E. Freschi and B. Lellmann. Understanding Prescriptive Texts: Rules and Logic as elaborated by the Mimamsa school. Accepted for publication in Confluence: Online Journal of World Philosophies
    5. M. Bongini, A. Ciabattoni and F. Montagna. Proof Search and Co-NP Completeness for Many-Valued Logics. Fuzzy Sets and Systems 292: 130-149 (2016)
    6. R. Kuznets and T. Studer Weak arithmetical interpretations for the Logic of Proofs. Journal of the IGPL , 24(3), pp 424-440, 2016
    7. L.M. Cabrer and H.A. Priestley. Natural dualities through product representations: bilattices and beyond. Accepted for publication in Studia Logica .
    8. B. Lellman and R. Kuznets. Grafting Hypersequents onto Nested Sequents. Journal of the IGPL. 24(3), pp. 375-423, 2016.
    9. L.M. Cabrer and D. Mundici. Classifying GL(n,Z^n)-orbits of points and rational subspaces. Accepted for publication in Discrete and Continuous Dynamical Systems
    10. R. Ramanayake Inducing syntactic cut-elimination for indexed nested sequents. Proceedings of the International Joint Conference on Automated Reasoning IJCAR 2016. LNCS.
    11. A. Ciabattoni Analytic Calculi for Non-Classical Logics: Theory and Applications. CSL 2016: 4:1-4:1
    12. A. Ciabattoni and F. Genco mbedding formalisms: hypersequents and two-level systems of rules. Proceedings of the Conference AIML 2016
    13. L.M. Cabrer, U. Rivieccio and R. Rodriguez . Lukasiewicz public announcement logic. Proceedings of the Conference Information Processing and Management of Uncertainty in Knowledge Based Systems
    14. B. Lellmann. Hypersequent Rules with Restricted Contexts for Propositional Modal Logics. Theoretical Computer Science , 656, pp. 76-105, 2016.


    1. N. Galatos and G. Metcalfe. Proof Theory for lattice-ordered groups. Accepted for publication in Annals of Pure and Applied Logic
    2. P. Baldi and A. Ciabattoni. Uniform proofs of standard completeness for extensions of first-order MTL. Theoretical Computer Science 603: 43-57 (2015)
    3. M. Fitting and R. Kuznets. Modal interpolation via nested sequents. Ann. Pure Appl. Logic 166(3): 274-305 (2015)
    4. R. Kuznets. Craig Interpolation via Hypersequents. In Concepts of Proof in Mathematics, Philosophy, and Computer Science, volume 6 of Ontos Mathematical Logic series of Ontos Verlag
    5. R. Ramanayake Non-commutative classical arithmetical sequent calculi are intuitionistic. Journal of the IGPL 24(3): 441-452.
    6. P. Baldi and K. Terui. Densification of FL chains via residuated frames. Accepted for publication in Algebra Universalis
    7. R. Ramanayake. Embedding the hypersequent calculus in the display calculus. J. of Logic and Computation, Volume 25, Issue 3, pp 921-942, 2015
    8. P. Baldi and A. Ciabattoni. Standard completeness for uninorm-based logics. IEEE International Symposium on Multiple-Valued Logic (ISMVL 2015)
    9. A. Ciabattoni, F. A. Genco, E. Freschi and B. Lellmann. Mimamsa Deontic Logic: Proof Theory and Applications. Tableaux 2015 LNCS
    10. B. Lellmann. Linear Nested Sequents, 2-sequents and Hypersequents. Tableaux 2015 LNCS
    11. B. Lellmann and E. Pimentel. Proof Search in Nested Sequent Calculi. LPAR 2015 LNCS
    12. A. Borg and R. Kuznets. Realization theorems for justification logics: Full modularity. Tableaux 2015 LNCS


    1. A. Ciabattoni, O. Lahav, L. Spendier and A. Zamansky. Taming Paraconsistent (and Other) Logics: An Algorithmic Approach. TOCL Vol. 16(1)
    2. B. Lellmann. Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications. IJCAR 2014
    3. A. Ciabattoni, R. Ramanayake and H. Wansing. Hypersequent and display calculi -- a unified perspective. Studia Logica Vol. 102(6), pp. 1245-1294
    4. R. Gore and R. Ramanayake Cut-elimination for weak Grzegorczyk logic Studia Logica Volume 102, Issue 1, pp 1-27
    5. P. Baldi. A note on standard completeness for some extensions of uninorm logic. Accepted for publication in Soft Computing
    6. A. Ciabattoni and L. Spendier. Tools for the investigation of substructural and paraconsistent logics. JELIA 2014 pp. 18-32


    1. A. Ciabattoni, P. Maffezioli and L. Spendier. Hypersequent and Labelled Calculi for Intermediate Logics, Proceedings of TABLEAUX 2013, PDF
    2. A. Avron, B. Konikowska, A. Zamansky. Cut-free sequent calculi for C-systems with generalized finite-valued semantics. J. Log. Comput. 23(3): 517-540 (2013) PDF
    3. M. Baaz, O. Lahav, A. Zamansky. Finite-valued Semantics for Canonical Labelled Calculi. J. Autom. Reasoning 51(4): 401-430 (2013) PDF
    4. P. Maffezioli and A. Naibo. Proof theory of epistemic logic of programs. Logic and Logical Philosophy. 2013
    5. A. Ciabattoni and R. Ramanayake. Structural extensions of display calculi: a general recipe. WOLLIC 2013.
    6. O. Lahav. From Frame Properties to Hypersequent Rules in Modal Logics. LICS 2013.
    7. A. Ciabattoni and F. Montagna. Proof theory for locally finite many-valued logics: semi-projective logics. Theoretical Computer Science, 480: 26-42 (2013).
    8. A. Ciabattoni, O. Lahav, L. Spendier and A. Zamansky. Automated Support for the Investigation of Paraconsistent and Other Logics. Proceedings of the Symposium on Logical Foundations in Computer Science 2013 (LFCS 2013). S. Artemov and A. Nerode (Eds.), LNCS.


    1. A. Ciabattoni, N. Galatos and K. Terui. Algebraic proof theory for substructural logics: cut-elimination and completions. Annals of Pure and Applied Logic. 163(3): 266-290 (2012).
    2. P. Baldi, A Ciabattoni and L. Spendier. Standard completeness for extensions of MTL: an automated approach. Workshop on Logic, Language, Information and Computation (WoLLIC 2012). L. Ong and R. de Queiroz (Eds.), LNCS 7456, 154-167. *Springer, Heidelberg (2012)*.
    3. M. Baaz, A Ciabattoni and C.G. Fermüller. Theorem proving for prenex Goedel logic with Delta: checking validity and unsatisfiability. Logical Methods for Computer Science 8(1), (2012).
    4. K. Chvalovsky, P. Cintula. Note on Deduction Theorems in Contraction-Free Logics. Mathematical Logic Quarterly 58(3), 236-243 (2012).
    5. P. Cintula, C. Noguera. The Proof by Cases Property and its Variants in Structural Consequence Relations. *To appear in Studia Logica*.
    6. O. Lahav. Non-deterministic Matrices for Semi-canonical Deduction Systems. Accepted to ISMVL 2012. IEEE, 79-84.
    7. P. Maffezioli and A. Naibo. Proof Theory of epistemic logic of programs. Logic and Logical Philosophy, The Nicolaus Copernicus University Press, Special issue dedicated to the Proceedings of the Fifth Conference: Non-Classical Logic. Theory and Applications, September 2729, 2012; Toru, Poland (2012).


    1. A. Ciabattoni, O. Lahav and A. Zamansky. Basic Constructive Connectives, Determinism and Matrix-based Semantics. Forthcoming in the Proceedings of Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2011).
    2. A. Ciabattoni, N. Galatos and K. Terui. MacNeille Completions of FL-algebras. Algebra Universalis 66(4), 405-420 (2011).