Proof systems for Geometric theories (PROGEO)
Resumo
We plan to study the problem of finding conservative extensions of first order logics. In this project we intend to establish a systematic procedure for adding geometric theories in both intuitionistic and classical logics, as well as to extend this procedure to bipolar axioms, a generalization of the set of geometric axioms. This way, we obtain proof systems for several mathematical theories, such as lattices, algebra and projective geometry, being able to reason about such theories using automated deduction.
Palavras-chave:
Sequent systems, Focusing, Bipoles
Referências
Chaudhuri, K. (2008). Focusing strategies in the sequent calculus of synthetic connectives. In Cervesato, I., Veith, H., and Voronkov, A., editors, Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings, volume 5330 of Lecture Notes in Computer Science, pages 467–481. Springer.
Danos, V., Joinet, J.-B., and Schellinx, H. (1995). LKT and LKQ: sequent calculi for second order logic based upon dual linear decompositions of classical implication. In Girard, J.-Y., Lafont, Y., and Regnier, L., editors, Advances in Linear Logic, number 222 in London Mathematical Society Lecture Note Series, pages 211–224. Cambridge University Press.
Dyckhoff, R. and Negri, S. (2015). Geometrisation of first-order logic. The Bulletin of Symbolic Logic, 21(2):123–163.
Gentzen, G. (1935a). Investigations into logical deduction. In Szabo, M. E., editor, The Collected Papers of Gerhard Gentzen, pages 68–131. North-Holland, Amsterdam.
Gentzen, G. (1935b). Untersuchungen über das logische schliessen. Mathematische Zeitschrift, 39:176–210.
Liang, C. and Miller, D. (2007). Focusing and polarization in intuitionistic logic. In Duparc, J. and Henzinger, T. A., editors, CSL 2007: Computer Science Logic, volume 4646 of LNCS, pages 451–465. Springer.
Liang, C. and Miller, D. (2009). Focusing and polarization in linear, intuitionistic, and classical logics. Theor. Comput. Sci., 410(46):4747–4768.
Marin, S., Miller, D., Pimentel, E., and Volpe, M. (2020). From axioms to synthetic inference rules via focusing. Available at https://drive.google.com/file/d/ 1_gNtKjvmxyH7T7VwpUD0QZtXARei8t5K/view.
Negri, S. (2003). Contraction-free sequent calculi for geometric theories with an application to Barr’s theorem. Arch. Math. Log., 42(4):389–401.
Negri, S. (2005). Proof analysis in modal logic. J. Philosophical Logic, 34(5-6):507– 544.
Negri, S. (2016). Proof analysis beyond geometric theories: from rule systems to systems of rules. J. Log. Comput., 26(2):513–537.
Negri, S. and von Plato, J. (1998). Cut elimination in the presence of axioms. Bulletin of Symbolic Logic, 4(4):418–435.
Negri, S. and von Plato, J. (2011). Proof Analysis - a contribution to Hilbert’s last problem. Cambridge University Press.
Simpson, A. K. (1994). The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, College of Science and Engineering, School of Informatics, University of Edinburgh.
Viganò, L. (2000). Labelled Non-Classical Logics. Kluwer Academic Publishers.
Danos, V., Joinet, J.-B., and Schellinx, H. (1995). LKT and LKQ: sequent calculi for second order logic based upon dual linear decompositions of classical implication. In Girard, J.-Y., Lafont, Y., and Regnier, L., editors, Advances in Linear Logic, number 222 in London Mathematical Society Lecture Note Series, pages 211–224. Cambridge University Press.
Dyckhoff, R. and Negri, S. (2015). Geometrisation of first-order logic. The Bulletin of Symbolic Logic, 21(2):123–163.
Gentzen, G. (1935a). Investigations into logical deduction. In Szabo, M. E., editor, The Collected Papers of Gerhard Gentzen, pages 68–131. North-Holland, Amsterdam.
Gentzen, G. (1935b). Untersuchungen über das logische schliessen. Mathematische Zeitschrift, 39:176–210.
Liang, C. and Miller, D. (2007). Focusing and polarization in intuitionistic logic. In Duparc, J. and Henzinger, T. A., editors, CSL 2007: Computer Science Logic, volume 4646 of LNCS, pages 451–465. Springer.
Liang, C. and Miller, D. (2009). Focusing and polarization in linear, intuitionistic, and classical logics. Theor. Comput. Sci., 410(46):4747–4768.
Marin, S., Miller, D., Pimentel, E., and Volpe, M. (2020). From axioms to synthetic inference rules via focusing. Available at https://drive.google.com/file/d/ 1_gNtKjvmxyH7T7VwpUD0QZtXARei8t5K/view.
Negri, S. (2003). Contraction-free sequent calculi for geometric theories with an application to Barr’s theorem. Arch. Math. Log., 42(4):389–401.
Negri, S. (2005). Proof analysis in modal logic. J. Philosophical Logic, 34(5-6):507– 544.
Negri, S. (2016). Proof analysis beyond geometric theories: from rule systems to systems of rules. J. Log. Comput., 26(2):513–537.
Negri, S. and von Plato, J. (1998). Cut elimination in the presence of axioms. Bulletin of Symbolic Logic, 4(4):418–435.
Negri, S. and von Plato, J. (2011). Proof Analysis - a contribution to Hilbert’s last problem. Cambridge University Press.
Simpson, A. K. (1994). The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, College of Science and Engineering, School of Informatics, University of Edinburgh.
Viganò, L. (2000). Labelled Non-Classical Logics. Kluwer Academic Publishers.
Publicado
26/08/2020
Como Citar
PIMENTEL, Elaine.
Proof systems for Geometric theories (PROGEO). In: WORKSHOP BRASILEIRO DE LÓGICA (WBL), 1. , 2020, Evento Online.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2020
.
p. 57-64.
ISSN 2763-8731.
DOI: https://doi.org/10.5753/wbl.2020.11459.
