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

• Author(s):
  • Pierre Letouzey (initial)
  • Laurent Théry (initial)
• Coq-community maintainer(s):
  • Karl Palmskog (@palmskog)
• License: GNU Lesser General Public License v2.1 or later
• Compatible Coq versions: Coq master (use the corresponding branch or release for other Coq versions)
• Additional dependencies: none
• Coq namespace: Stalmarck.Algorithm
• Related publication(s):
  • Formalizing Stålmarck's Algorithm in Coq doi:10.1007/3-540-44659-1_24

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

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.

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

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.

Priority of connectives, from lower to higher:

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

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).

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

stalmarck 1 tests/ztwaalf1_be
Tautology