full screen background image

Publications

PhD Thesis

    Paolo Baldi ( Standard completeness: proof-theoretic and algebraic methods ), defended August 2015
    Francesco Genco (Intermediate logics and concurrent lambda-calculi: a proof theoretic approach) , defended May 2019
    Lara Spendier (Tools for the Investigation of Non-classical Logics ), defended June 2015

    2019

  1. R. Ramanayake . Extended Kripke lemma and decidability for hypersequent substructural logics. LICS 2020
  2. F. Aschieri, A. Ciabattoni and F. A. Genco . A typed parallel lambda-calculus via 1-depth intermediate proofs. Proceedings of LPAR 2020.
  3. F. Aschieri, A. Ciabattoni and F. A. Genco . On the Concurrent Computational Content of Intermediate Logics Accepted for publication to Theoretical Computer science.
  4. F. Aschieri, F. A. Genco . Par means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs. Proceedings of POPL 2020.
  5. K. van Berkel, T. Lyon, and F. Olivieri. A Decidable Multi-Agent Logic for Reasoning about Actions, Instruments, and Norms. Proceedings of CLAR 2020.
  6. T. Lyon . Syntactic Cut-Elimination for Intuitionistic Fuzzy Logic via Linear Nested Sequents. Proceedings of LFCS 2020.
  7. T. Lyon, A. Tiu, R. Gore, and R. Clouston. Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents. Proceedings of CSL 2020
  8. T. Lyon . On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems. Proceedings of LFCS 2020
  9. A. Ciabattoni, T. Lang, and R. Ramanayake . Bounded Sequent Calculi for Non-Classical Logics via Hypersequents. Proceedings of Tableaux 2019.
  10. B. Lellmann, E. Pimentel, and and R. Ramanayake . Sequentialising Nested Systems. Proceedings of Tableaux 2019
  11. K. van Berkel and T. Lyon . A Neutral Temporal Deontic STIT Logic. Proceedings of LORI 2019.
  12. T. Lyon and K. van Berkel. Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics. Proceedings of PRIMA 2019.
  13. F. Aschieri, S. Hetzl, D. Weller. Expansion Trees with Cut, Mathematical Structures in Computer Science, to appear
  14. F. Aschieri. Natural Deduction and Normalization Proofs for the Intersection Type Discipline, Proceedings of Intersection Types and Related Systems 2018, EPTCS, to appear
  15. K. van Berkel and T. Lyon. Cut-free Calculi and Relational Semantics for Temporal STIT logics. Proceedings of JELIA 2019.

    16. 2018

  16. F. Aschieri, A. Ciabattoni, F. Genco. Classical Proofs as parallel Programs. Proceedings of GANDALF 2018
  17. F. Aschieri. On Natural Deduction for Herbrand Constructive Logics III: The Strange Case of the Intuitionistic Logic of Constant Domains. Proceedings Seventh International Workshop on Classical Logic and Computation. EPTCS 281, pp. 1--9. 2018
  18. E. Pimentel A Semantical View of Proof Systems. Proceedings of Wollic 2018
  19. B. Lellmann and R. Kuznets. Interpolation for Intermediate Logics via Hyper- and Linear Nested Sequents. Proceedings of AIML 2018
  20. A. Ciabattoni and F. Genco. Hypersequents and Systems of Rules: Embeddings and Applications. ACM Transaction on Computational Logic , 19(2): 11:1-11:27 (2018).
  21. A. Ciabattoni, T. Lyon, and R. Ramanayake. From Display to Labelled Proofs for Tense Logics. Proceedings of LFCS 2018.
  22. R. Kuznets. Through an Inference Rule, Darkly . Accepted to Postproceedings of Humboldt-Kolleg "Proof Theory as Mathesis Universales", 2018. To be published in Synthese Library
  23. R. Kuznets. Multicomponent Proof-theoretic Method for Proving Interpolation Properties. Annals of Pure and Applied Logic. To appear
  24. C. Olarte, E. Pimentel and C. Rocha. Proving Structural Properties of Sequent Systems in Rewriting Logic. In Proceedings of WRLA, 2018.
  25. K. Chaudhuri, J. Despeyroux, C. Olarte and E. Pimentel. Hybrid Linear Logic. Mathematical Structures in Computer Science. To appear
  26. C. Nalon and D. Pattinson. A Resolution-Based Calculus for Preferential Logics. In Proceedings of the 9th International Joint Conference on Automated Reasoning, IJCAR 2018, Oxford, UK. LNCS, Springer, 2018. To appear.

    27. 2017

    1. F. Aschieri, A. Ciabattoni, F. Genco. Goedel Logic: From Natural Deduction to Parallel Computation. Proceedings of LICS 2017
    2. A. Ciabattoni, N. Galatos and K. Terui. Algebraic proof theory: hypersequents and hypercompletions. Annals of Pure and Applied Logic. 168(3): 693-737, 2017.
    3. 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
    4. A. Ciabattoni and R. Ramanayake. Bunched Hypersequent Calculi for Distributive Substructural Logics. Proceedings of LPAR-21
    5. P. Baldi, A. Ciabattoni and F. Giulisano. Standard completeness for extensions of IMTL. Proceedings of FUZZ-IEEE 2017: International Conference on Fuzzy Systems

    2016

    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.

    2015

    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

    2014

    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

    2013

    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.

    2012

    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).

    2011

    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).