Description

Le calcul epsilon de Hilbert est une formulation sans quantificateurs de la logique du premier ordre. En raison de sa syntaxe complexe, il n'a pas suscité beaucoup d'intérêt en vérification formelle. Cependant, le calcul epsilon peut offrir un gain de vitesse non élémentaire par rapport à des calculs plus classiques. Avec ce projet, je souhaite appliquer ce gain de vitesse au domaine de la démonstration de théorèmes automatisée et interactive.

Compétences requises

Le candidat retenu devra connaître la logique du premier ordre et sa théorie de la démonstration.

Bibliographie

[1] Juan P. Aguilera and Matthias Baaz. Unsound Inferences Make Proofs Shorter. The Journal of Symbolic Logic, 84(1):102-122, 2019.

[2] Andrea Aler Tubella, Alessio Guglielmi, and Benjamin Ralph. Removing cycles from proofs. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic (CSL), volume 82 of Leibniz International Proceedings in Informatics (LIPIcs), pages 9:1-17. Schloss Dagstuhl, Leibniz-Zentrum für Informatik, 2017.

[3] Cameron Allett. Non-elementary compression of FIrst-order proofs in deep inference using epsilon-terms. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'24, New York, NY, USA, 2024. Association for Computing Machinery.

[4] Matthias Baaz and Anela Lolic. A Globally Sound Analytic Calculus for Henkin Quantifiers. Logical Foundations of Computer Science: International Symposium, LFCS 2020, pages 128-143, 2020.

[5] Matthias Baaz and Anela Lolic. Epsilon calculus provides shorter cut-free proofs, 2024.

[6] Kai Brünnler. Cut elimination inside a deep inference system for classical predicate logic. Studia Logica, 82(1):51-71, 2006.

[7] Paola Bruscoli and Alessio Guglielmi. On the proof complexity of deep inference. ACM Transactions on Computational Logic, 10(2):1-34, 2009. Article 14.

[8] Paola Bruscoli, Alessio Guglielmi, Tom Gundersen, and Michel Parigot. A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae. In LPAR-16, volume 6355 of LNCS, pages 136-153. Springer-Verlag, 2010.

[9] Alessio Guglielmi. Towards a new proof theory of quantification. EECS Theory Seminar, Queen Mary, London, 2020.

[10] David Hilbert and Paul Bernays. Grundlagen der Mathematik, volume 2. Springer Verlag, 2 edition, 1968.

[11] Emil Jerábek. Proof complexity of the cut-free calculus of structures. Journal of Logic and Computation, 19(2):323-339, 2009.

[12] Georg Moser and Richard Zach. The epsilon calculus and herbrand complexity.
Studia Logica, 82:133-155, 2006.

[13] Benjamin Ralph. Modular Normalisation of Classical Proofs. PhD thesis, University of Bath, 2019.

[14] Lutz Strassburger and Alessio Guglielmi. A system of interaction and structure IV: The exponentials and decomposition. ACM Trans. Comput. Log., 12(4):23, 2011.

Mots clés

Le calcul epsilon, recherche de preuves, théorie de la démonstration