Logic and Mechanized Reasoning

This repository is designed to accompany the course by the same name. See also:

• the textbook (in progress): https://avigad.github.io/lamr
• a PDF version of the textbook: https://avigad.github.io/lamr/logic_and_mechanized_reasoning.pdf
• the course home page: https://www.cs.cmu.edu/~mheule/15311-s25/

This repository contains a supporting library and files containing examples from the textbook that you can edit and experiment with.

The course requires the Lean 4 programming language and theorem prover, as well as three additional automated reasoning tools: CaDiCaL (a SAT solver), Z3 (an SMT solver), and Vampire (a resolution theorem prover).

There are two ways for you to use the software and supporting libraries.

Option 1: use this repository on your computer

1. Install Lean 4 and VS Code following these instructions.

2. Make sure you have git installed.

3. If you have not logged in since you installed Lean and Mathlib, then you may need to first type source ~/.profile or source ~/.bash_profile depending on your OS.

4. Open a terminal, navigate to the directory where you want to clone the repository, and type:

   git clone git@github.com:avigad/lamr.git
   cd lamr
   lake exe cache get
   lake build
   

   This fetches the repository and builds it.

5. Launch VS Code by typing code . or start VS Code some other way and open the lamr folder. Note that you have to open the top level lamr repository folder, not any other folder.

From the file explorer on the left-hand side, you can now open .lean files such as the ones in the directory LAMR/Examples. We recommend putting your own files in the User folder and leaving the original content intact.

Note that the files in LAMR/bin are Linux binaries of automated reasoning tools. If you are using MacOS or Windows you need to replace these with appropriate versions. (See below.)

You can update to a newer version of the repository by typing the following in the lamr repository folder:

  git pull
  lake exe cache get
  lake build

Option 2: use this repository with Github Codespaces

You can also use this repository with Lean running in the cloud using Github Codespaces. This requires a Github account. If you are signed in to Github, click here: https://codespaces.new/avigad/lamr.

Make sure the Machine type is 4-core, and then press Create codespace. This creates a virtual machine in the cloud, and installs Lean and Mathlib. Click on the extensions icon in the sidebar (the four squares), and install then Lean 4 extension. Then type lake build in the terminal to build the local files.

You can update the repository by opening a terminal in the browser and typing git pull followed by lake exe cache get and lake build as above.

Codespaces offers a certain number of free hours per month. When you are done working, press Ctrl/Cmd+Shift+P on your keyboard, start typing stop codespace, and then select Codespaces: Stop Codespace from the list of options. If you forget, don't worry: the virtual machine will stop itself after a certain amount of time of inactivity.

To restart a previous workspace, visit https://github.com/codespaces.

To use the automated reasoning tools

The LAMR/bin folder in the repository contains Linux binaries for CaDiCaL, Z3, CVC4, CVC5, and Vampire. We provide procedures for calling them from Lean, and the LAMR/Examples folder has some examples. If you are using the course with Gitpod or locally with Linux, the external tools will hopefully work out of the box. If you are using OS/X or Windows, however, you will have to obtain or build the relevant binaries on your own and replace the ones in LAMR/bin. You can find information on how to do that here:

• CaDiCaL
• Z3
• CVC4
• CVC5
• Vampire

Building CaDiCaL for Windows seems difficult. You do not need all three SMT solvers; any one of Z3, CVC4, or CVC5 will do.