以命题逻辑的消解或归结（resolution）证明为例，所谓消解规则就是从子句和得出子句的过程。一个合取范式是永假式，当且仅当从该合取范式的所有子句开始，可以用消解规则得出空子句。这个过程中所有符号的二进制编码长度之和就是证明的长度，通常也可以用证明过程中符号的个数或者子句的个数作为证明的长度，它们彼此都是多项式相关的。通常考虑一族命题的渐近证明复杂性。以鸽巢原理（即鸽笼原理）为例，鸽巢原理说若把只鸽子放入个鸽巢，则至少有一个鸽巢内要放两只以上的鸽子。用布尔变元表示第只鸽子是否放入第个鸽巢。用合取范式表示个鸽子中每个鸽子至少放入一个鸽巢并且个鸽巢中每个鸽巢至多放入一个鸽子。显然是永假式。利用瓶颈法或插值法，可以证明的任何消解证明的长度都是指数长的，即长度的。

美国计算机科学家S.A.库克（Stephen Arthur Cook，1939-12-14～　　）和他的学生R.A.雷克豪（Robert A.Reckhow）在1979年精确定义了命题证明系统（propositional proof system）。所谓命题证明系统，就是从到的多项式时间可计算的满射，这里是构成潜在证明的有穷符号串的集合，是全体永真式的集合。是多项式时间可计算的，这意味着当给出对于公式的一个证明时，可以在证明长度的多项式时间内验证的正确性。如果对于任何能证明的公式，都存在着长度不超过f的长度的多项式的证明，则该证明系统是多项式有界的（p-bounded）。如果对于任何能证明的公式，都能在最短证明的长度的多项式时间内计算出来，则该证明系统是可自动化的（automatizable）。S.A.库克和R.A.雷克豪定义了一个称为弗雷格系统（Frege System）的命题证明系统，建议把证明弗雷格系统证明复杂性的超多项式下界作为证明的一个途径。因为是完全的，所以弗雷格系统是多项式有界的当且仅当，弗雷格系统是可自动化的当且仅当。目前只对较弱的证明系统（比如上述的消解证明系统等）证明出了指数下界。