TableauxRocq: A Library of Free-Variable Tableaux in Rocq

This repository aims at providing a library for (i) formalizing free-variable tableaux proofs in Rocq, and (ii) outputing optimized tableaux proofs for fast certification.

Table of contents

• Documentation
• Installation and Local Compilation
• Extraction of the Proof Checker
• Outputing Proofs using TableauxRocq

Documentation

Documentation gets automatically deployed for each version of TableauxRocq. The documentation following the development version (e.g., tracking the master branch) can be accessed at jrosain.github.io/TableauxRocq/master.
Documentation for a specific version is linked on the associated release/ branch.

Installation and Local Compilation

Requirements

This project depends on Rocq. It is compiled using Rocq 9.1.1 in the CI, but is compatible with the following versions of Rocq:

• rocq-core 9.0.0 with rocq-stdlib 9.0.0
• rocq-core 9.0.1 with rocq-stdlib 9.0.0
• rocq-core 9.1.0 with rocq-stdlib 9.1.0
• rocq-core 9.1.1 with rocq-stdlib 9.1.0

There are two ways of compiling the project.

Nix Installation (recommended)

A fully-reproducible setup is achieved using flake.nix and shell.nix files and a pinned version of nixpkgs. We ensure that the project always compiles under this pinned version of Rocq. One simply needs to use nix-shell to fetch and install the correct version of Rocq.

The library is available using Nix flakes. It can be added to the inputs using the following lines:

tr = {
  url = "git+https://github.com/jrosain/TableauxRocq";
  inputs.nixpkgs.follows = "nixpkgs";
};

The corresponding output is in tr.packages.${system}.rocqPackages.rocq-tableaux. We currently support the systems x86_64-linux and aarch64-linux.

opam Installation

Another way of installing the dependencies of the project is via opam, using one of the pairs listed above. For instance, if one wants the latest compatible version of Rocq, they have to enter the following commands:

opam pin add rocq-core 9.1.1
opam pin add rocq-stdlib 9.1.0

ocamlfind is also necessary but should be already installed.

Compilation

After installing the dependencies, the following command configures and compiles the project:

make

In order to use the library globally on your computer, you can install it:

make install

If you are a developer of the library and simply want to configure (i.e., generate or re-generate the Makefiles), you can use the config target:

make config

Documentation

The documentation can be generated via the doc target of the Makefile:

make doc

Warning: this commands needs pandoc to generate the index file out of the README.md. Note that it is included in the nix configuration file, so if you use nix, it should work out of the box.

Extraction of the Proof Checker

By default, running make will extract ML code to the folder checker. In order to compile this code, one needs dune (version 3) and OCaml (version 5). For Nix users, these softwares are already furnished by the shell.nix file. This can be deactivated by setting the input withExtraction to false.

If TableauxRocq has been added to one's flakes (as described in the Nix installation section), the binary of the proof checker can be obtained by adding the package tr.packages.${system}.poulet in one's configuration.

Otherwise, it can be compiled by using dune build in the checker folder. The whole process is streamlined by the poulet target of the Makefile, i.e., make poulet will extract the proof checker and compile poulet with dune.

Afterwards, you can find the binary as:

• poulet in the root of the repository if you used make poulet,
• checker/_build/default/bin/poulet.exe if you built it using dune.

Outputing Proofs using TableauxRocq

If you develop a tableau-based automated theorem prover, you can certify your proofs using TableauxRocq. There are two ways of doing that.

Outputing TPTP-like Proofs (Recommended)

We define a TPTP-like grammar (fully documented in GRAMMAR) as our proof format. It can be used by the certified OCaml checker poulet, that we get by extracting TableauxRocq algorithm to check proofs.

The binary can be compiled from source using make poulet (see Extraction of the Proof Checker).

Examples of proofs can be found in the GRAMMAR, and in the different files of the test-suite (see e.g., the folder devtools/tests/basic).

Outputing Rocq Code

One can directly export proofs in Rocq. TableauxRocq's core is based on a minimal syntax and proof system, but we provide an extended syntax, semantics and tableau proofs in the ExtendedSyntax file, that supports the full first-order syntax. Then, to get started on developing an output, a showcase of the different types of rules are done in the following files:

• drinker: a proof of the drinker paradox $\exists x.\ P(x) \to \forall y.\ P(y)$ using two different Skolemization methods: inner and outer Skolemization. This illustrates how to use a formula multiple times, and how inner Skolemization is better than outer Skolemization.
• branching: a proof of the formula $\exists x.\ P(x) \to P(a) \land P(b)$. Here, both the inner and outer Skolemization proofs are also showcased even though they have the same number of rules applied. Nevertheless, this gives a nice example of a branching rule.

The folder devtools/tests/rocq has examples for the application of other rules, but these files are not documented.