Propositional proof system

In propositional calculus and proof complexity a propositional proof system (pps), also called a Cook–Reckhow propositional proof system, is a system for proving classical propositional tautologies. == Mathematical definition == Formally a pps is a polynomial-time function P whose range is the set of all propositional tautologies (denoted TAUT).

Source: Wikipedia — Propositional proof system (CC BY-SA 4.0)