Skip to content

Certified implementation in Coq of Stålmarck's algorithm for proving tautologies [maintainer=@palmskog]

License

Notifications You must be signed in to change notification settings

coq-community/stalmarck

Repository files navigation

Stalmarck

Docker CI Nix CI Contributing Code of Conduct Zulip DOI

A two-level approach to prove tautologies using Stålmarck's algorithm in Coq.

Meta

Building and installation instructions

The easiest way to install the latest released version of Stalmarck is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-stalmarck

To instead build and install manually, do:

git clone https://github.com/coq-community/stalmarck.git
cd stalmarck
make   # or make -j <number-of-cores-on-your-machine> 
make install

Documentation

This project is composed of:

  • A Coq proof of correctness of the algorithm, as described in the paper A Formalization of Stålmarck's Algorithm in Coq, published in the proceedings of TPHOLs 2000.
  • an implementation of the algorithm. With respect to the paper, this implementation is completely functional and can be used inside Coq.
  • A reflected Coq tactic staltac that uses the extracted code to compute an execution trace; the trace checker is then called inside Coq.
  • A standalone checker program stalmarck which takes as input a formula in textual format and reports whether it can be certified as a tautology.

See algoRun.v for examples how to use the algorithm inside Coq, and see StalTac_ex.v for examples how to use the reflected tactic.

Tautology Checker

The src directory contains the code for a standalone tautology checker using the implementation of Stålmarck's algorithm extracted from Coq.

Running the checker

stalmarck <level> <file>

where:

  • <level> is an integer controling depth of dilemma. Usual values:
    • 0: does only propagation.
    • 1: dilemma upon one variable at the same time.
    • 2: dilemma can be done upon two variables at the same time; more than 2 may take very long.
  • <file> is the file containing the boolean formula.

Boolean formula syntax

Concept Syntax
Comments // (reading is suspended until the end of the line)
Variable any alphanumeric sequence plus the character _
Not ~
And &
Or #
Implication ->
Equivalence <->
Parentheses ( )
True value <T>
False value <F>

Priority of connectives, from lower to higher:

  • <->, -> (associate to the right)
  • # (associates to the left)
  • & (associates to the left)
  • ~

Output

The only interesting output is Tautology (and exit code 0). The other output is Don't know (and exit code 1): either the formula is not a tautology, or it is one but the program cannot conclude this (insufficient level).

Example

An example file with a tautology (tests/ztwaalf1_be) is included, and can be checked as follows:

stalmarck 1 tests/ztwaalf1_be
Tautology