It is unworthy of excellent men to lose hours like slaves in the labour of calculations which could be safely relegated to anyone else if machines were used.

—Gottfried Wilhelm Leibniz, 1671

Calculation becomes deduction.

—Gottlob Frege

fregerator is an automated theorem prover. It extends Frege's above quote. Calculation becomes deduction, and deduction becomes computation, just like everything else.

fregerator is currently a work in progress and not suitable for production use.

Released under the GPLv3.

• Early versions of the codebase are inspired by some of the work on Benedict Eastaugh's hatt.

I have benefited greatly from many different books and papers:

• The Handbook of Practical Logic and Automated Reasoning has proved to be an invaluable resource for when it comes to translating results in logic into algorithms.
• The representation of first-order logic was informed by Kenneth Knowles's article in The Monad Reader, "First-Order Logic à la Carte".
• Frank Wilson's dissertation on building a theorem prover in Haskell.
• Laurence Edward Day's paper "Implementing a Propositional Logic Theorem Prover in Haskell".