Abstract. Formalising algebraic structures (groups, rings, fields, vector spaces, lattices, . . . ) is known to be challenging task which is often under- taken by exploiting various kind of extra-logical mechanisms (axiomatic classes, modules, locales, coercions, . . . ) provided by most modern theo- rem provers. We want to explore an alternative strategy, where algebraic structures are implemented via a deep embedding of mathematical formulas and are managed as first class objects in the HOL theory. Along the way, we provide a mechanism of generalised conversions, which extends Paulson’s conversions by allowing to compute with equivalence relations. We developed generalised conversions to support rewriting in our system, but they can be used independently and may have an interest in its own.

A symbolic approach to abstract algebra in HOL Light / Marco, Maggesi. - ELETTRONICO. - (2015), pp. 1-4.

A symbolic approach to abstract algebra in HOL Light

Marco Maggesi
2015

Abstract

Abstract. Formalising algebraic structures (groups, rings, fields, vector spaces, lattices, . . . ) is known to be challenging task which is often under- taken by exploiting various kind of extra-logical mechanisms (axiomatic classes, modules, locales, coercions, . . . ) provided by most modern theo- rem provers. We want to explore an alternative strategy, where algebraic structures are implemented via a deep embedding of mathematical formulas and are managed as first class objects in the HOL theory. Along the way, we provide a mechanism of generalised conversions, which extends Paulson’s conversions by allowing to compute with equivalence relations. We developed generalised conversions to support rewriting in our system, but they can be used independently and may have an interest in its own.
2015
Marco, Maggesi
File in questo prodotto:
File Dimensione Formato  
2015-07-15-FMM-symbolic.pdf

accesso aperto

Tipologia: Versione finale referata (Postprint, Accepted manuscript)
Licenza: Tutti i diritti riservati
Dimensione 174.03 kB
Formato Adobe PDF
174.03 kB Adobe PDF

I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificatore per citare o creare un link a questa risorsa: https://hdl.handle.net/2158/1105060
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact