Image de couverture de livre

The Directed Van Kampen Theorem in Lean

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Basold, Henning, Bruin, Peter, Lawson, Dominique
Format:	Preprint
Publié:	2023
Sujets:	Logic in Computer Science 03B35 F.4.1; F.1.2
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

Thoughts on sub-Turing interactive computability
par: Japaridze, Giorgi
Publié: (2024)

On the computational properties of ambivalent sets and functions
par: Normann, Dag, et autres
Publié: (2026)

Bennett's Conjecture in Lean 4: Counter-Models for the PSR-Reducibility of Spinoza's Propositions V and XIV
par: Nakamura, Yuki
Publié: (2026)

Evaluating Autoformalization Robustness via Semantically Similar Paraphrasing
par: Moore, Hayden, et autres
Publié: (2025)

Universal Gluing and Contextual Choice: Categorical Logic and the Foundations of Analytic Approximation
par: Santacana, Andreu Ballus
Publié: (2025)

A Proof-Theoretic Approach to the Semantics of Classical Linear Logic
par: Barroso-Nascimento, Victor, et autres
Publié: (2025)

Glivenko's theorems from an ecumenical perspective
par: Pereira, Luiz Carlos, et autres
Publié: (2026)

A Resolution-Based Interactive Proof System for UNSAT
par: Czerner, Philipp, et autres
Publié: (2024)

Internal Effectful Forcing in System T
par: Escardo, Martin H., et autres
Publié: (2025)

Complexity Results in Team Semantics: Nonemptiness Is Not So Complex
par: Anttila, Aleksi, et autres
Publié: (2025)

Proof Compression via Subatomic Logic and Guarded Substitutions
par: Barrett, Victoria, et autres
Publié: (2025)

Propositional Dynamic Logic has Craig Interpolation: a tableau-based proof
par: Borzechowski, Manfred, et autres
Publié: (2025)

A Modular Lean 4 Framework for Confluence and Strong Normalization of Lambda Calculi with Products and Sums
par: Ramos, Arthur, et autres
Publié: (2025)

Deducibility in the full Lambek calculus with weakening is HAck-complete
par: Greati, Vitor, et autres
Publié: (2024)

Hypersequent Calculi Have Ackermannian Complexity
par: Balasubramanian, A. R., et autres
Publié: (2026)

A Coherence Construction for the Propositional Universe
par: Huang, Xu
Publié: (2024)

Type Theory with Explicit Universe Polymorphism (revised and extended version)
par: Bezem, Marc, et autres
Publié: (2022)

Computability of the Hahn-Banach Theorem Revisited
par: Brattka, Vasco, et autres
Publié: (2026)

Normal forms in cubical type theory
par: Huang, Xu
Publié: (2026)

Finite Hilbert systems for Weak Kleene logics
par: Greati, Vitor, et autres
Publié: (2024)

Knowability as continuity: a topological account of informational dependence
par: Baltag, Alexandru, et autres
Publié: (2024)

Axiomatizing the Logic of Ordinary Discourse
par: Greati, Vitor, et autres
Publié: (2024)

Generating proof systems for three-valued propositional logics
par: Greati, Vitor, et autres
Publié: (2024)

Belief in Simplicial Complexes
par: Sink, Philip, et autres
Publié: (2025)

Reasoning Around Paradox with Grounded Deduction
par: Ford, Bryan
Publié: (2024)

A Note on Proper Relational Structures
par: Bjorndahl, Adam, et autres
Publié: (2025)

Continuous and algebraic domains in univalent foundations
par: de Jong, Tom, et autres
Publié: (2024)

Cut elimination for propositional cyclic proof systems with fixed-point operators
par: Hori, Hiromasa, et autres
Publié: (2023)

Agent Interpolation for Knowledge
par: Bílková, Marta, et autres
Publié: (2025)

Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic
par: Santo, José Espírito, et autres
Publié: (2020)

Tao's Equational Proof Challenge Accepted (Technical Report)
par: Kondylidou, Lydia, et autres
Publié: (2026)

Inclusion with repetitions and Boolean constants -- implication problems revisited
par: Häggblom, Matilda
Publié: (2025)

Axiomatization of approximate exclusion
par: Häggblom, Matilda
Publié: (2024)

Axiomatizing approximate inclusion
par: Häggblom, Matilda
Publié: (2025)

Fixed-Point Theorems and the Ethics of Radical Transparency: A Logic-First Treatment
par: Alpay, Faruk, et autres
Publié: (2025)

Separation Logic of Generic Resources via Sheafeology
par: van Starkenburg, Berend, et autres
Publié: (2025)

Extracting total Amb programs from proofs
par: Berger, Ulrich, et autres
Publié: (2023)

First-Order Fischer Servi Logic
par: Christensen, Ahmee
Publié: (2024)

How to play the Accordion: Uniformity and the (non-)conservativity of the linear approximation of the λ-calculus (extended version)
par: Cerda, Rémy, et autres
Publié: (2023)

Complexity of some modal logics of density (extended version)
par: Balbiani, Philippe, et autres
Publié: (2025)