[isabelle] new AFP entry: Residuated Lattices
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] new AFP entry: Residuated Lattices
- From: Gerwin Klein <Gerwin.Klein at nicta.com.au>
- Date: Thu, 16 Apr 2015 16:07:19 +0000
- Accept-language: en-AU, en-US
- Thread-index: AQHQeF9qoJyCJKLXVkmuhxHfyvvuxA==
- Thread-topic: new AFP entry: Residuated Lattices
by Victor B. F. Gomes and Georg Struth
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.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
This archive was generated by a fusion of
Pipermail (Mailman edition) and