Welcome to residuated-binars’s documentation!

Generating Algebraic Structures with Isabelle

Attention

If you’re looking for a reproducible example for AITP 2021 paper, find it here.

Attention

The project is inactive.

This package serves for generating and validating examples of different algebraic structures using Isabelle proof assistant.

Dependencies

Make sure that an installation of Isabelle is on the $PATH

How to Install

The best way to install residuated-binars is to use pip:

pip install residuated-binars

Alternatively, one can use Docker:

docker build -t residuated-binars https://github.com/inpefess/residuated-binars.git
docker run -it --rm -p 8888:8888 residuated-binars jupyter-lab --ip=0.0.0.0 --port=8888 --no-browser

Finally, one can run it on Binder

How to Use

See examples/residuated-binars-example.ipynb.

Contents:

• Distributivity Laws in Residuated Binars with Involution
• Additional Files Descriptions
  • DistributiveCase.thy
  • notebooks/binars.pkl
  • notebooks/rb-check.ipynb
  • notebooks/another-check.ipynb
• Algebraic Structures
  • Axiom Checkers
  • Parser
  • Algebraic Structure
  • Lattice
  • Residuated Binar
  • Abelian Group
  • Boolean Ring
  • Pseudo-weak-\(R_0\) Algebra
  • Pseudo-\(R_0\) Algebra
• Using Isabelle to Generate Algebraic Structures
  • Constants
  • Generate Theories
  • Script for adding a task
  • Check Assumptions
  • Filter Theories
  • Use Nitpick
  • Short scripts useful for other sub-modules

Indices and tables

• Index

• Module Index

• Search Page