Formalization of the fundamental group in untyped set theory using auto2

DOI10.1007/978-3-319-66107-0_32zbMath1468.68331arXiv1707.04757OpenAlexW2736867616WikidataQ129449803 ScholiaQ129449803MaRDI QIDQ5915787

Bohua Zhan

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

zbMATH Keywords

fundamental groupset theoryIsabelle

Mathematics Subject Classification ID

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

• Isabelle
• Isabelle/HOL
• Mizar
• z3
• Isabelle/ZF
• ProofPower
• HOL Light
• Metamath
• AUTO2
• IsarMathLib

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