Residuated Lattices

Victor B. F. Gomes 📧 and Georg Struth 📧

April 15, 2015

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

The theory of residuated lattices, first proposed by Ward and Dilworth, is formalised in Isabelle/HOL. This includes concepts of residuated functions; their adjoints and conjugates. It also contains necessary and sufficient conditions for the existence of these operations in an arbitrary lattice. The mathematical components for residuated lattices are linked to the AFP entry for relation algebra. In particular, we prove Jonsson and Tsinakis conditions for a residuated boolean algebra to form a relation algebra.

License

BSD License

Topics

Session Residuated_Lattices

Depends on

Cite

× 
@article{Residuated_Lattices-AFP,
  author  = {Victor B. F. Gomes and Georg Struth},
  title   = {Residuated Lattices},
  journal = {Archive of Formal Proofs},
  month   = {April},
  year    = {2015},
  note    = {\url{https://isa-afp.org/entries/Residuated_Lattices.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: