Some Axioms for Mathematics
| Autor: | Blanqui, Frédéric, Dowek, Gilles, Grienenberger, Émilie, Hondet, Gabriel, Thiré, François |
|---|---|
| Přispěvatelé: | Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Nomadic Labs |
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: |
interoperabilty
dependent types Type theory Logic axiomatic theory [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Theory of computation → Type theory Theory of computation → Logic rewriting Logical framework [MATH.MATH-LO]Mathematics [math]/Logic [math.LO] TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computer Science::Logic in Computer Science Theory of computation → Equational logic and rewriting Computer Science::Databases |
| Zdroj: | FSCD 2021-6th International Conference on Formal Structures for Computation and Deduction FSCD 2021-6th International Conference on Formal Structures for Computation and Deduction, Jul 2021, Buenos Aires / Virtual, Argentina. ⟨10.4230/LIPIcs.FSCD.2021.20⟩ |
| DOI: | 10.4230/LIPIcs.FSCD.2021.20⟩ |
| Popis: | The λΠ-calculus modulo theory is a logical framework in which many logical systems can be expressed as theories. We present such a theory, the theory {U}, where proofs of several logical systems can be expressed. Moreover, we identify a sub-theory of {U} corresponding to each of these systems, and prove that, when a proof in {U} uses only symbols of a sub-theory, then it is a proof in that sub-theory. LIPIcs, Vol. 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), pages 20:1-20:19 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|