  The development of   -->proof theory-->  can be naturally divided into: the prehistory of the notion of proof  in ancient logic and mathematics; the discovery by   Frege  that mathematical proofs, and not only the propositions of  mathematics, can (and should) be represented in a logical system;   Hilbert's old axiomatic proof theory;  failure of the aims of Hilbert through Gödel's incompleteness  theorems; Gentzen's creation of the two main types of logical systems of contemporary proof theory, natural deduction and sequent calculus  (see the entry on   automated reasoning);  applications and extensions of natural deduction and sequent  calculus, up to the computational interpretation of natural deduction and its connections with computer science.