Exploring the structure of an algebra text with locales

DOI10.1007/s10817-019-09537-9zbMath1468.68277OpenAlexW2993571361WikidataQ114689846 ScholiaQ114689846MaRDI QIDQ2209550

Clemens Ballarin

Publication date: 2 November 2020

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-019-09537-9

zbMATH Keywords

localescase studyabstract algebramodule systemIsabelletheorem prover

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

A modular first formalisation of combinatorial design theory ⋮ Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types ⋮ Multiple-inheritance hazards in dependently-typed algebraic hierarchies ⋮ Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem ⋮ A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory ⋮ A formalization of the Smith normal form in higher-order logic

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• Automath
• Locales
• Archive Formal Proofs
• Secondary Sylow
• Jacobson_Basic_Algebra

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A mechanized proof of the basic perturbation lemma
• Locales: a module system for mathematical theories
• Mechanisation of AKS Algorithm: Part 1 – The Main Theorem
• Constructive Type Classes in Isabelle
• Local Theory Specifications in Isabelle/Isar
• Institutions: abstract model theory for specification and programming
• Defining functions on equivalence classes
• Canonical Structures for the Working Coq User
• Types for Proofs and Programs