Forward Chaining and Safe Saturation in Abella



This webpage contains some supporting material for the paper:

“Designing a safe forward chaining tactic using productive proofs” by Kaustuv Chaudhuri, Arunava Gantait, and Dale Miller,

which has been submitted to a conference (draft from May 2025).

You may browse the following developments on-line. To run them yourself, you will need the saturate branch of Abella, which you can install using OPAM as follows.

$ git clone https://github.com/abella-prover/abella.git
$ cd abella
$ git checkout saturate
$ opam pin abella . # note the final period and say "yes" when prompted

Examples

Last updated: