Skip to content

Verifying encodings into propositional logic in Lean

Notifications You must be signed in to change notification settings

ccodel/verified-encodings

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

30 Commits
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Verified encodings in Lean

This is a project by Cayden Codel, advised by Jeremy Avigad and Marijn Heule. It intends to formally verify encodings of Boolean functions, cardinality constraints, and other methods of specifying mathematical problems in propositional logic.

Building locally

You can install Lean following the instructions at https://leanprover-community.github.io/get_started.html#regular-install.

Assuming you have Lean installed, you can fetch and build this repository as follows:

  leanproject get ccodel/verified-encodings
  cd verified-encodings
  leanproject build

You can then open folder in VS Code and browse the files.

Using Gitpod

If you have an account with Gitpod, you can instead browse the repository in your browser, running Lean in the cloud. If you don't have an account with Gitpod, clicking the button will prompt you to create one.

Open in Gitpod

Gitpod offers 50 free hours of workspace time every month. When you are done, choose "Stop workspace" from the menu in the upper left corner to stop the clock. Alternatively, Gitpod will stop it for you after 30 minutes, or 3 minutes after you close the browser window or tab.

About

Verifying encodings into propositional logic in Lean

Resources

Stars

Watchers

Forks

Packages

No packages published

Languages