Publications
PhD Thesis

Paolo Baldi
( Standard completeness: prooftheoretic and algebraic methods ), defended August 2015

F. Aschieri, F. A. Genco .
Par means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs.
Proceedings of POPL 2020.

T. Lyon .
Syntactic CutElimination for Intuitionistic Fuzzy Logic via Linear Nested Sequents. Proceedings of LFCS 2020.

T. Lyon .
T. Lyon, A. Tiu, R. GorĂ©, and R. Clouston. Syntactic Interpolation for Tense Logics and BiIntuitionistic Logic via Nested Sequents. Proceedings of CSL 2020

T. Lyon .
On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems. Proceedings of LFCS 2020

A. Ciabattoni, T. Lang, and R. Ramanayake .
Bounded Sequent Calculi for NonClassical Logics via Hypersequents. Proceedings of Tableaux 2019.

B. Lellmann, E. Pimentel, and and R. Ramanayake .
Sequentialising Nested Systems. Proceedings of Tableaux 2019

K. van Berkel and T. Lyon . A Neutral Temporal Deontic STIT Logic. Proceedings of LORI 2019.

T. Lyon and K. van Berkel.
Automating Agential Reasoning: ProofCalculi and Syntactic Decidability
for STIT Logics. Proceedings of PRIMA 2019.

F. Aschieri, S. Hetzl, D. Weller.
Expansion Trees with Cut, Mathematical Structures in Computer Science, to appear
 F. Aschieri.
Natural Deduction and Normalization Proofs for the
Intersection Type Discipline, Proceedings of Intersection Types and Related Systems 2018, EPTCS,
to appear

K. van Berkel and T. Lyon.
Cutfree Calculi and Relational Semantics for Temporal STIT logics. Proceedings of JELIA 2019.
 F. Aschieri, A. Ciabattoni, F. Genco.
Classical Proofs as parallel Programs.
Proceedings of GANDALF 2018
 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. 19. 2018
 E. Pimentel
A Semantical View of Proof Systems.
Proceedings of Wollic 2018
 B. Lellmann and R. Kuznets.
Interpolation for Intermediate Logics via Hyper and Linear Nested Sequents.
Proceedings of AIML 2018
 A. Ciabattoni and F. Genco.
Hypersequents and Systems of Rules: Embeddings and Applications. ACM Transaction on Computational Logic ,
19(2): 11:111:27 (2018).
 A. Ciabattoni, T. Lyon, and R. Ramanayake.
From Display to Labelled Proofs for Tense Logics. Proceedings of LFCS 2018.
 R. Kuznets.
Through an Inference Rule, Darkly .
Accepted to Postproceedings of HumboldtKolleg "Proof Theory as Mathesis Universales", 2018.
To be published in Synthese Library
 R. Kuznets.
Multicomponent Prooftheoretic Method for Proving Interpolation Properties.
Annals of Pure and Applied Logic. To appear
 C. Olarte, E. Pimentel and C. Rocha.
Proving Structural Properties of Sequent Systems in Rewriting Logic.
In Proceedings of WRLA, 2018.
 K. Chaudhuri, J. Despeyroux, C. Olarte and E. Pimentel.
Hybrid Linear Logic. Mathematical Structures in Computer Science. To appear
 C. Nalon and D. Pattinson.
A ResolutionBased Calculus for Preferential Logics.
In Proceedings of the 9th International Joint Conference on Automated
Reasoning, IJCAR 2018, Oxford, UK. LNCS, Springer, 2018. To appear.
 F. Aschieri, A. Ciabattoni, F. Genco.
Goedel Logic: From Natural Deduction to Parallel Computation.
Proceedings of LICS 2017
 A. Ciabattoni, N. Galatos and K. Terui.
Algebraic proof theory: hypersequents and hypercompletions.
Annals of Pure and Applied Logic. 168(3): 693737, 2017.
 A. Ciabattoni, B, Lellmann, C. Olarte and E. Pimentel.
From cutfree calculi to automated deduction: the case of bounded contraction.
Accepted for publication in ENTCS
 A. Ciabattoni and R. Ramanayake.
Bunched Hypersequent Calculi for Distributive Substructural Logics. Proceedings of
LPAR21
 P. Baldi, A. Ciabattoni and F. Giulisano.
Standard completeness for extensions of IMTL. Proceedings of
FUZZIEEE 2017: International Conference on Fuzzy Systems
 A. Ciabattoni and R. Ramanayake.
Power and limits of structural display rules.
ACM Trans. Comput. Log. 17(3): 17 .
 M. Baaz and A. Ciabattoni.
Proof theory of witnessed Goedel logic: a negative result.
Journal of Logic and Computation 26(1): 5164 (2016)
 R. Ramanayake
Noncommutative classical arithmetical sequent calculi are intuitionistic.
Journal of the IGPL , 24(3), pp 441452, 2016
 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
 M. Bongini, A. Ciabattoni and F. Montagna.
Proof Search and CoNP Completeness for ManyValued Logics. Fuzzy Sets and Systems 292: 130149 (2016)
 R. Kuznets and T. Studer
Weak arithmetical interpretations for the Logic of Proofs.
Journal of the IGPL , 24(3), pp 424440, 2016
 L.M. Cabrer and H.A. Priestley.
Natural dualities through product representations: bilattices and beyond.
Accepted for publication in Studia Logica .
 B. Lellman and R. Kuznets.
Grafting Hypersequents onto Nested Sequents. Journal of the IGPL. 24(3), pp. 375423, 2016.
 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
 R. Ramanayake
Inducing syntactic cutelimination for indexed nested sequents.
Proceedings of the International Joint Conference on Automated Reasoning IJCAR 2016. LNCS.
 A. Ciabattoni
Analytic Calculi for NonClassical Logics: Theory and Applications.
CSL 2016: 4:14:1
 A. Ciabattoni and F. Genco
mbedding formalisms: hypersequents and twolevel systems of rules.
Proceedings of the Conference AIML 2016
 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
 B. Lellmann.
Hypersequent Rules with Restricted Contexts for Propositional Modal Logics. Theoretical Computer Science ,
656, pp. 76105, 2016.
 N. Galatos and G. Metcalfe.
Proof Theory for latticeordered groups. Accepted for publication in Annals of Pure and Applied Logic
 P. Baldi and A. Ciabattoni.
Uniform proofs of standard completeness for extensions of firstorder MTL. Theoretical Computer Science
603: 4357 (2015)
 M. Fitting and R. Kuznets. Modal interpolation via nested sequents.
Ann. Pure Appl. Logic 166(3): 274305 (2015)
 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
 R. Ramanayake
Noncommutative classical arithmetical sequent calculi are intuitionistic.
Journal of the IGPL 24(3): 441452.
 P. Baldi and K. Terui. Densification of FL chains via residuated frames.
Accepted for publication in Algebra Universalis
 R. Ramanayake.
Embedding the hypersequent calculus in the display calculus.
J. of Logic and Computation, Volume 25, Issue 3, pp 921942, 2015
 P. Baldi and A. Ciabattoni.
Standard completeness for uninormbased logics. IEEE International Symposium on MultipleValued Logic (ISMVL 2015)
 A. Ciabattoni, F. A. Genco, E. Freschi and B. Lellmann.
Mimamsa Deontic Logic: Proof Theory and Applications. Tableaux 2015 LNCS
 B. Lellmann.
Linear Nested Sequents, 2sequents and Hypersequents. Tableaux 2015 LNCS
 B. Lellmann and E. Pimentel.
Proof Search in Nested Sequent Calculi. LPAR 2015 LNCS
 A. Borg and R. Kuznets.
Realization theorems for justification logics: Full modularity. Tableaux 2015 LNCS
 A. Ciabattoni, O. Lahav, L. Spendier and A. Zamansky.
Taming Paraconsistent (and Other) Logics: An Algorithmic Approach. TOCL Vol. 16(1)
 B. Lellmann. Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications. IJCAR 2014
 A. Ciabattoni, R. Ramanayake and H. Wansing. Hypersequent and display calculi  a unified perspective. Studia Logica Vol. 102(6), pp. 12451294
 R. Gore and R. Ramanayake Cutelimination for weak Grzegorczyk logic Studia Logica Volume 102, Issue 1, pp 127
 P. Baldi. A note on standard completeness for some extensions of uninorm logic. Accepted for publication in Soft Computing
 A. Ciabattoni and L. Spendier. Tools for the investigation of substructural and paraconsistent logics. JELIA 2014 pp. 1832
 A. Ciabattoni, P. Maffezioli and L. Spendier. Hypersequent and Labelled Calculi for Intermediate Logics, Proceedings of TABLEAUX 2013, PDF
 A. Avron, B. Konikowska, A. Zamansky. Cutfree sequent calculi for Csystems with generalized finitevalued semantics. J. Log. Comput. 23(3): 517540 (2013) PDF
 M. Baaz, O. Lahav, A. Zamansky. Finitevalued Semantics for Canonical Labelled Calculi. J. Autom. Reasoning 51(4): 401430 (2013) PDF
 P. Maffezioli and A. Naibo. Proof theory of epistemic logic of programs. Logic and Logical Philosophy. 2013
 A. Ciabattoni and R. Ramanayake. Structural extensions of display calculi: a general recipe. WOLLIC 2013.
 O. Lahav. From Frame Properties to Hypersequent Rules in Modal Logics. LICS 2013.
 A. Ciabattoni and F. Montagna. Proof theory for locally finite manyvalued logics: semiprojective logics. Theoretical Computer Science, 480: 2642 (2013).
 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.
 A. Ciabattoni, N. Galatos and K. Terui. Algebraic proof theory for substructural logics: cutelimination and completions. Annals of Pure and Applied Logic. 163(3): 266290 (2012).
 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, 154167. *Springer, Heidelberg (2012)*.
 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).
 K. Chvalovsky, P. Cintula. Note on Deduction Theorems in ContractionFree Logics. Mathematical Logic Quarterly 58(3), 236243 (2012).
 P. Cintula, C. Noguera. The Proof by Cases Property and its Variants in Structural Consequence Relations. *To appear in Studia Logica*.
 O. Lahav. Nondeterministic Matrices for Semicanonical Deduction Systems. Accepted to ISMVL 2012. IEEE, 7984.
 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: NonClassical Logic. Theory and Applications, September 2729, 2012; Toru, Poland (2012).
 A. Ciabattoni, O. Lahav and A. Zamansky. Basic Constructive Connectives, Determinism and Matrixbased Semantics. Forthcoming in the Proceedings of Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2011).
 A. Ciabattoni, N. Galatos and K. Terui. MacNeille Completions of FLalgebras. Algebra Universalis 66(4), 405420 (2011).
Francesco Genco (Intermediate logics and concurrent lambdacalculi: a proof theoretic approach) , defended May 2019
Lara Spendier (Tools for the Investigation of Nonclassical Logics ), defended June 2015
2019
2018
2017
2016
2015
2014
2013
2012
2011