Frege system

In proof complexity, a Frege system is a propositional proof system whose proofs are sequences of formulas derived using a finite set of sound and implicationally complete inference rules. Frege systems (more often known as Hilbert systems in general proof theory) are named after Gottlob Frege.

The name "Frege system" was first defined by Stephen Cook and Robert Reckhow, and was intended to capture the properties of the most common propositional proof systems.