![[Structural Proof Theory]](spt.png)
|
![[Structural Proof Theory]](pa.png)
|
The electronic versions of articles available here may differ from the published versions.
|
|
|
65. PRONOM: proof-search and countermodel generation for non-normal modal logics (with Tiziano Dalmonte, Nicola Olivetti and Gianluca Pozzato). AIIA 2019, 18th International Conference of the I\ talian Association for Artificial Intelligence, pdf of final version.
64. Uniform labelled calculi for conditional and counterfactual logics (with Marianna Girlando and Giorgio Sbardolini). R. Iemhoff et al. (eds), WoLLIC 2019, LNCS 11541, pdf of final version.
63. Proof theory for quantified monotone modal logics (with Eugenio Orlandelli). Logic Journal of the IGPL, https://doi.org/10.1093/jigpal/jzz015, pdf of final version.
62. From mathematical axioms to mathematical rules of proof: recent developments in proof analysis (with Jan von Plato). Philosophical Transactions of the Royal Society A, in press, pdf of final version.
61. Non-normal modal logics: bi-neighbourhood semantics and its labelled calculi (with Tiziano Dalmonte and Nicola Olivetti). Advances in Modal Logic 2018, pdf of final version.
60. Counterfactual logic: labelled and internal calculi, two sides of the same coin? (with Marianna Girlando and Nicola Olivetti). Advances in Modal Logic 2018, pdf of final version.
59. Conditional beliefs: from neighbourhood semantics to sequent calculus (with Marianna Girlando, Nicola Olivetti, and Vincent Risch). To appear in the Review of Symbolic Logic, pdf of final version.
58. The intensional side of algebraic-topological representation theorems. Synthese, pdf of final version.
57. Proof theory for non-normal modal logics: The neighbourhood formalism and basic results, pdf file, IfCoLog Journal of Logics and their Applications, Mints' memorial issue, vol. 4(4), May 2017, pp. 1241-1286. correction note.
56. Non-normal modal logics: a challenge to proof theory. In In P. Arazim and T. Lavicka (eds) The Logica Yearbook 2016, pp. 125-140, College Publications, pdf of final version\ .
55. Dyckhoff, R. and S. Negri. Commentary on Grigori Mints' ``Classical and Intuitionistic Geometric Logic''. IfCoLog Journal of Logics and their Applications, Mints' memorial issue, vol. 4(4), May 2017, pp. 1235-1239Ã?pdf.
54. A system of proof for Lewis counterfactual, with G. Sbardolini. In L. Felline et al. (eds) New Directions in Logic and the Philosophy of Science, pp. 189-203, College Publications, 2016.
53. The logic of conditional beliefs: neighbourhood semantics and sequent calculus, with M. Girlando, N. Olivetti, and V. Risch, AiML 2016, pdf file.
52. Le direzioni della ricerca logica in Italia: Teoria strutturale della dimostrazione. In H. Hosni, G. Lolli, and C. Toffalori (eds) "Le direzioni della ricerca logica in Italia". Edizioni della Normale, Pisa, pp. 221-253, 2015, pdf file.
51. Glivenko sequent classes in the light of structural proof theory. Archive for Mathematical Logic, vol. 55, pp 461-473, 2016, pdf file.
50. A sequent calculus for preferential conditional logic based on neighbourhood semantics, with Nicola Olivetti. Proceedings of Tableaux 2015, pdf file.
49. Proof analysis for Lewis counterfactuals, with Giorgio Sbardolini. The Review of Symbolic Logic, vol. 9, pp. 44-75, 2016, pdf file.
48. Cut elimination in sequent calculi with implicit contraction, with a conjecture on the origin of Gentzen's altitude line construction, with Jan von Plato. In Dieter Probst and Peter Schuster (eds.), "Concepts of Proof in Mathematics, Philosophy, and Computer Science". Ontos Mathematical Logic. Walter de Gruyter, Berlin, pp. 269-290, 2016, pdf file.
47. Geometrization of first-order logic, with Roy Dyckhoff. The Bulletin of Symbolic Logic , vol. 21, pp. 123-163, 2015, pdf file.
46. Proofs and countermodels in non-classical logics. Logica Universalis, vol. 8, pp. 25-60, 2014, pdf file.
45. Proof analysis beyond geometric theories: from rule systems to systems of rules. Journal of Logic and Computation, vol. 27, pp. 513-537, 2016 pdf file.
44. On the duality of proofs and countermodels in labelled sequent calculi (extended abstract of invited talk), in D. Galmiche and D. Larchey Wendling (eds) Automated Reasoning with Analytic Tableaux and Related Methods: 22th International Conference, Tableaux 2013, LNAI 8123, Springer, pdf file.
43. A cut-free sequent system for Grzegorczyk logic with an application to the Gödel-McKinsey-Tarski embedding. With Roy Dyckhoff, Journal of Logic and Computation, vol. 26, pp. 169-187, 2016 pdf file.
42. Meaning in use, with Jan von Plato, in H. Wansing (ed) Dag Prawitz on Proofs and Meaning, Trends in Logic, Springer, pp. 239-257, 2015, pdf file.
41. Countermodels from Sequent Calculi in Multi-Modal Logics, with Deepak Garg and Valerio Genovese, proceedings of LICS 2012, IEEE Computer Society, pp. 315-324, 2012, pdf file, technical report.
40. The Church-Fitch knowability paradox in the light of structural proof theory, with Paolo Maffezioli and Alberto Naibo, Synthese, vol. 190, pp. 2677-2716, 2013, pdf file .
39. Proof analysis in intermediate logics (with Roy Dyckhoff), Archive for Mathematical Logic, vol. 51, pp. 71-92, 2012, pdf file .
Using labelled formulae, a cut-free sequent calculus for intuitionistic propositional logic is presented, together with an easy cut-admissibility proof; both extend to cover, in a uniform fashion, all intermediate logics characterised by frames satisfying conditions expressible by one or more geometric implications. Each of these logics is embedded by the Gödel-McKinsey-Tarski translation intoan extension of S4. Faithfulness of the embedding is proved in a simple and general way by constructive proof-theoretic methods, without appeal to semantics other than in the explanation of the rules.
38. A proof theoretical perspective on Public Announcement Logic, with Paolo Maffezioli, Logic and Philosophy of Science, vol. 9, pp. 49-59, 2011, pdf file .
37. Proof theory for modal logic, Philosophy Compass, 6/8 (2011), pp. 523-538, pdf file.
The axiomatic presentation of modal systems and the standard formulations of natural deduction and sequent calculus for modal logic are reviewed, together with the difficulties that emerge with these approaches. Generalizations of standard proof systems are then presented. These include, among others, display calculi, hypersequents, and labelled systems, with the latter surveyed from a closer perspective.
36. A Gentzen-style analysis of Public Announcement Logic, (with Paolo Maffezioli), in X. Arrazola and M. Ponte (eds) Proceedings of the International Workshop on Logic and Philosophy of Knowledge, Communication and Action, pp. 293-313, University of the Basque Country Press, 2010, pdf file .
35. Does the deduction theorem fail for modal logic? (with Raul Hakli), Synthes\ e, vol. 187, pp. 849-867, 2012, pdf file .
34. Reasoning about collectively accepted group beliefs (with Raul Hakli), to appear in Herzig, A. and E. Lorini (eds) ``Logical Methods for Social Concepts'' Journal of Philosophical Logic, vol. 40, pp. 531-555, 2011. pdf file .
33. Kripke completeness revisited, in G. Primiero and S. Rahman (eds.), "Acts of Knowledge - History, Philosophy and Logic", College Publications, 2009, pdf file.
The evolution of completeness proofs for modal logic with respect to the possible world semantics is studied starting from an analysis of Kripke's original proofs from 1959 and 1963. The critical reviews by Bayart and Kaplan and the emergence of Henkin-style completeness proofs are detailed. It is shown how the use of a labelled sequent system permits a direct and uniform completeness proof for a wide variety of modal logics that is close to Kripke's original arguments but without the drawbacks of Kripke's or Henkin-style completeness proofs. It is detailed in particular how a process of failed proof search in a labelled sequent calculus with invertible rules directly provides a countermodel to the endsequent.
32. Proof theory for distributed knowledge (with Raul Hakli), Computational Logic in Multi-Agent Systems, Springer Lecture Notes in Artificial Intelligence, vol. 5405, pp. 100--116, Springer, 2008, pdf file .
31. Decidability for Priorean Linear Time using a Fixed-Point Labelled Calculus (with Bianca Boretti), Lecture Notes in Computer Science, vol. 5607, Proceedings of Tableaux 2009, pdf file .
A labelled sequent calculus is proposed for Priorean linear time logic, a modal logic with two possibility- and two necessity-like operators, a serial accessibility relation and an infinitary rule of transitive closure. The rules of the calculus are defined in a cumulative way and reflect a natural closure algorithm derived from the fixed-point properties of the temporal operators. All the rules of the system are finitary, but proofs may contain infinite branches. Soundness and completeness of the calculus are stated with respect to a notion of provability based on a condition on derivation trees: A sequent is provable if and only if no branch leads to a 'fulfilling sequent', the syntactical counterpart of a countermodel for an invalid sequent. Decidability is proved through a terminating proof search procedure, with an exponential bound to the branches of derivation trees for valid sequents, calculated on the length of the characteristic temporal formula of the endsequent. The paper illustrates a very general methods of establishing decidability in a constructive way through its application to linear temporal logic. The use of labels permits to formalize model-theoretic arguments within a proof-theoretical approach and to unify proofs of completeness and decidability by the generation of Kripke countermodels.
30. On the finitization of Priorean linear time (with Bianca Boretti), in D'Agostino et al. (eds) New Essays in Logic and Philosophy of Science, College Publications, London, 2010, pdf file .
29. Equality in the presence of apartness: An application of structural proof analysis to intuitionistic axiomatics (with Bianca Boretti), in "Constructivism: Mathematics, Logic, Philosophy and Linguistics" G. Ronzitti and G. Heinzmann (eds), Philosophia Scientiae, pp. 61-79, Cahier special 6, 2006.
28. Proof analysis in non-classical logics, in "Logic Colloquium '05: Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, Athens, Greece, July 28-August 3, 2005". C. Dimitracopoulos, L. Newelski, D. Normann, and J. Steel (eds) ASL Lecture Notes in Logic, vol. 28, pp. 107-128, pdf file
27. Proof analysis in modal logic, Journal of Philosophical Logic, vol 34, pp. 507--544, 2005. pdf file .
26. The duality of classical and constructive notions and proofs (with Jan von Plato), in "From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics" (L. Crosilla, P. Schuster, eds.), Oxford University Press, pp. 149--161, 2005. pdf file .
25. Decision methods for linearly ordered Heyting algebras (with Roy Dyckhoff), Archive for Mathematical Logic, vol 45, pp. 411-422, 2006, pdf file .
24. Permutability of rules for linear lattices , in C. Calude and H. Ishihara (eds) "Constructivity, Computability, and Logic" Journal of Universal Computer Science, vol 11, no. 12, pp. 1986-1995, 2005. pdf file.
23. Proof systems for lattice theory, written with Jan von Plato, Mathematical Structures in Computer Science, vol. 14, pp. 507--526, 2004. pdf file .
22. Permutability of rules in lattice theory, written with Jan von Plato, Algebra Universalis, vol. 48 (2002), pp. 473-477. pdf file .
21. Proof theoretical analysis of order relations, written with with Jan von Plato and Thierry Coquand, Archive for Mathematical Logic, vol. 43, pp. 297--309, 2004. pdf file .
20. Contraction-free sequent calculi for geometric theories, with an application to Barr's theorem, Archive for Mathematical Logic, vol. 42 (2003), pp. 389--401. pdf file, Correction note dvi file.
19. Varieties of linear calculi, Journal of Philosophical Logic, vol 31, pp. 569--590, 2002. ps, dvi, pdf file .
18. A sequent calculus for constructive ordered fields. Abstract. In "Reuniting the antipodes, Constructive and Nonstandard Views of the Continuum", P. Schuster et al. eds, pp. 143-155, Kluwer, Dordrecht, 2001. pdf file .
17. Admissibility of structural rules for extensions of contraction-free sequent calculi, written with Roy Dyckhoff, Logic Journal of the IGPL, vol. 9, no. 4, 2001 . pdf file .
16. Sequent calculus in natural deduction style, written with Jan von Plato, Abstract, pdf file . The Journal of Symbolic Logic, vol. 66, pp. 1803-1816, 2001.
15. Admissibility of structural rules for contraction-free systems of intuitionistic logic, written with Roy Dyckhoff, 1998. Abstract, pdf file . The Journal of Symbolic Logic, 65, (December 2000), pp. 1499--1518.
14. A normalizing system of natural deduction for intuitionistic linear logic, Archive for Mathematical Logic, vol. 41, pp.789--810, 2002. pdf file .
13. Cut elimination in the presence of axioms, (written with Jan von Plato), The Bulletin of Symbolic Logic, vol. 4, pp. 418-435, 1998, pdf file .
12. Sequent calculus proof theory of intuitionistic apartness and order relations, Archive for Math ematical Logic, vol. 38, no. 8, pp. 521-547, 1999. Abstract, pdf file .
11. From Kripke Models to Algebraic Counter-valuations, written with Jan von Plato, 1997. Abstract. In " Tableaux '98", Automated Reasoning with Analytic Tableaux and related methods, Harrie de Swart ed., LNAI 1397, pp. 247.270, 1998, pdf file .
10. Continuous domains as formal spaces , Mathematical Structures in Computer Science, vol. 12, pp. 19-52, 2002. Correction note dvi file.
9. Continuous lattices in formal topology, 1997. In Lecture Notes in Computer Science, E. Gimenez and C. Paulin (eds), selected papers of the Types meeting, Aussois, 1996, LNCS 1512, pp. 333-353, Springer, 1998. Full article just rescued (on 13.1.2009) from my old PowerBook!
8. The generalized Riemann integral on locally compact spaces , written with Abbas Edalat. Topology and its Applications, vol. 89, pp. 121--150, 1998. Abstract, dvi.gz file .
7. The generalized Riemann integral on locally compact spaces (extended abstract), written with Abbas Edalat, in ``Advances in Theory and Formal Methods of Computing'', A. Edalat, S. Jourdan and G. McCusker (eds), Imperial College Press, London, pp. 73-84, 1996.
6. The Hahn-Banach Theorem in Type Theory, written with Jan Cederquist and Thierry Coquand, in ``Twenty-Five Years of Constructive Type Theory'', G. Sambin and J. Smith (eds), pp. 57-72, 1998, Oxford University Press. Abstract, dvi.gz file .
5. A constructive proof of the Heine-Borel covering theorem for formal reals , written with Jan Cederquist, in ``Types for Proofs and Programs'', S. Berardi and M. Coppo (eds), Lecture Notes in Computer Science 1158, pp. 62-75, Springer Verlag, 1996. Abstract, ps.gz file ..
4. Tychonoff's theorem in the framework of formal topologies , written with Silvio Valentini, The Journal of Symbolic Logic, 62,4, pp. 1315-1332, 1997. You can see a summary here .
3. The continuum as a formal space, written with Daniele Soravia, Archive for Mathematical Logic , vol. 38, no. 7, pp. 423-447, 1999. Summary , ps file .
2. Stone bases, alias the constructive content of Stone representation ( ps , dvi), pdf), in ``Logic and Algebra'', A. Ursini and P. Agliano' (eds), Dekker, New York, pp. 617-636, 1996.
1. Semantical observations on the embedding of Intuitionistic Logic into Intuitionistic Linear Logic ( ps.gz ), Mathematical Structures in Computer Science, vol. 5, pp. 41-68, Cambridge University Press, 1995. You can see a summary here .