> Detailanzeige

Fellin, Giulio [Verfasser:in]; Negri, Sara [Verfasser:in]; Orlandelli, Eugenio [Verfasser:in] ; Giulio Fellin and Sara Negri and Eugenio Orlandelli [Mitwirkende:r]

Constructive Cut Elimination in Geometric Logic

Literatur-
verwaltung

Zur
Merkliste

Lösche von
Merkliste

Per Whatsapp teilen

Schließen

Merkliste



Sie können Bookmarks mittels Listen verwalten, loggen Sie sich dafür bitte in Ihr SLUB Benutzerkonto ein.
  • Medientyp: Sonstige Veröffentlichung; E-Artikel; Elektronischer Konferenzbericht
  • Titel: Constructive Cut Elimination in Geometric Logic
  • Beteiligte: Fellin, Giulio [Verfasser:in]; Negri, Sara [Verfasser:in]; Orlandelli, Eugenio [Verfasser:in]
  • Erschienen: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022
  • Sprache: Englisch
  • DOI: https://doi.org/10.4230/LIPIcs.TYPES.2021.7
  • Schlagwörter: Geometric theories ; sequent calculi ; constructive cut elimination ; axioms-as-rules ; infinitary logic
  • Entstehung:
  • Anmerkungen: Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
  • Beschreibung: A constructivisation of the cut-elimination proof for sequent calculi for classical and intuitionistic infinitary logic with geometric rules - given in earlier work by the second author - is presented. This is achieved through a procedure in which the non-constructive transfinite induction on the commutative sum of ordinals is replaced by two instances of Brouwer’s Bar Induction. Additionally, a proof of Barr’s Theorem for geometric theories that uses only constructively acceptable proof-theoretical tools is obtained.
  • Zugangsstatus: Freier Zugang