Publication:5915787: Difference between revisions
From MaRDI portal
Publication:5915787
Created automatically from import240129110113 |
EloiFerrer (talk | contribs) m EloiFerrer moved page Formalization of the fundamental group in untyped set theory using auto2 to Formalization of the fundamental group in untyped set theory using auto2: Duplicate |
(No difference)
| |
Latest revision as of 13:48, 2 May 2024
DOI10.1007/978-3-319-66107-0_32zbMath1468.68331arXiv1707.04757OpenAlexW2736867616WikidataQ129449803 ScholiaQ129449803MaRDI QIDQ5915787
Publication date: 4 January 2018
Published in: Journal of Automated Reasoning, Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1707.04757
Homotopy groups, general; sets of homotopy classes (55Q05) Mechanization of proofs and logical operations (03B35) Axiomatics of classical set theory and its fragments (03E30) Formalization of mathematics in connection with theorem provers (68V20)
Related Items (4)
Computational logic: its origins and applications ⋮ Formalising Mathematics in Simple Type Theory ⋮ Semantics of Mizar as an Isabelle object logic ⋮ First steps towards a formalization of forcing
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Set theory for verification. I: From foundations to functions
- Set theory for verification. II: Induction and recursion
- The James construction and \(\pi _4(\mathbb{S}^{3})\) in homotopy type theory
- AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic
- π n (S n ) in Homotopy Type Theory
- Mizar’s Soft Type System
- Efficient E-Matching for SMT Solvers
- Hammering towards QED
- Canonical Structures for the Working Coq User
- Alternative Aggregates in Mizar
This page was built for publication: Formalization of the fundamental group in untyped set theory using auto2
