### 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

- Mathematics/Algebra

### Session Residuated_Lattices

- Residuated_Lattices
- Residuated_Boolean_Algebras
- Involutive_Residuated
- Action_Algebra
- Action_Algebra_Models
- Residuated_Relation_Algebra

### Depends on

- Relation Algebra

### Auto-related entries

- A Verified Efficient Implementation of the Weighted Path Order
- The Hales–Jewett Theorem
- Irrational numbers from THE BOOK
- Compositional BD Security
- The Safely Composable DOM

## Cite

×

Residuated_Lattices-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 28, 2019 : Isabelle2019
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Apr 16, 2015 : Isabelle2014