Verified and Optimized Implementation of Orthologic Proof Search

This repository contains the formalization in Coq of the main result of Orthologic with Axioms (the cut elimination theorem for orthologic), and the implementation of an algorithm deciding orthologic inequalities, optimized using memoization and reference equality: The optimized algorithm is proven correct, and lifted to a Coq tactic using reflection. Independent proof search and normalization tactic implmented directly in OCaml are also provided.

The theorems and tactics are available as a plugin.

Requirements:

This formalization has been carried using Coq 8.18, Ocaml 5.3 and Dune 3.8. Using opam, run:

$ opam install dune.3.8.2 coq.8.18.0

Building the project

Build and verify the project using (takes a couple minutes):

$ dune build

You can also try the plugin by running:

$ coqtop -R _build/default/theories/ OLCoq -I _build/default/src/

and then

Coq < Require Import OLCoq.OLPlugin.

Installing the plugin

To install the plugin locally on your machine and use it in your own projects, run

$ opam pin --yes git@github.com:SimonGuilloud/orthologic-coq.git#main

or clone the repository and run at root

$ opam pin --yes ./

Tutorial

A short introduction to the plugin can be found in theories/Tutorial.v.

Reference Paper

Verified and Optimized Implementation of Orthologic Proof Search (Preprint, CAV 2025)

Benchmarks

Benchmarks where generated according to Main.scala using Scala and can be regenerated using sbt run. Benchmarks can be found in theories/olsolve_bench and theories/oltauto_bench. The raw results of the benchmarks are in bench.2025-01-31 and oltauto.bench.2025-02-01. They can be reevaluated with (takes arround 1 hour on a Intel Core i9-13900K CPU with 64GB RAM)

make solve-bench

and

make tauto-bench

To ease replication, this will run each benchmark only once. The results we report in the paper are the median of 5 runs. This can be changed line 82 of the theories/OL_Bench.v file.

Plots are plotted using plot.py.

Note that the objective of the first benchmark is to demonstrate that the asymptotic behaviour is as expected from the theory (results in lines.pdf) and the objective of the second benchmark is to show practical improvements over Coq's built-in solver for propositional logic, btauto (results in OCaml+n+btauto.pdf). The key corectness property of the artifact is validation by Coq, which is verified with dune build.