flypig.co.uk

Daeducer

A simple First Order Logic proof checker and generator that follows the approach from the Forall x: Calgary book on formal logic.

The tool can check proofs you enter or use machine learning models to automatically generate valid proofs. Valid proofs can be saved out and reloaded as lemmas, which can be used to simplify the construction of subsequent proofs.

Daeducer is an interactive terminal application. Once executed you can enter commands to build up valid proofs in the Fitch style using the rules as described in the Forall x: Calgary "Introduction to Formal Logic" by P.D. Magnus et al.

Daeducer includes an LLM harness which, given a suitable model, can generate proofs automatically. By combining this proof generation with its proof checking capability, Daeducer is able to guarantee that proofs produced this way are correct.

Using Qwen 3.5 35B A3B (a mixture-of-experts reasoning model) the tool is able to successfully answer all of the exercises in Forall x: Calgary and reproduce all of the examples without the need for human intervention.

Daeducer is written in C, and makes use of the Symbolic logic library and the llama.cpp inference engine. Building it from source is pretty straightforward. The proof-checking capability will run fine on a low-end CPU, but for proof generation you'll need a decent GPU in order to get acceptable performance. See the git repository for details about how you can built it from source.

This was written as a personal side-project to complement work being done in the Logic Reading Group at the Alan Turing Institute. The group saw us working through and in some areas beyond the text of Forall x: Calgary.

Licence

Daeducer is released under the AGPL 3.0.

Source code

The source code is available on Codeberg.