Added
- Dockerfile for building the prover.
- Explanation of how to build and run the prover using Docker.
- A link to the development repository in the README so releases can be found from the AFP distribution.
Fixed
- A bug that caused the completeness test runner to crash.
- A bug in proof extraction of consecutive Delta rules (see below).
The bug in proof extraction occurred when several Delta rules were applied in the same prover round, and caused generated function names to not be fresh beginning with the second Delta rule of the round. The remainder of the proof was unaffected, starting with the first
Ext rule after the Alpha-Delta phase.
The bug was due to the fact that the fresh name generated by each Delta rule was not carried forward internally in the round, but only "re-discovered" after the end of the phase.
The bug did not affect the prover algorithm, only the generation of proof certificates. Verification of proof certificates for formulas affected by the bug would fail despite the prover finding a proof, since the proof certificate would not contain a valid proof.