1樓：rainoftime
似乎並沒有直接貢獻...
Mathematical logic..
證明論創始人，提出自然演繹（Natural deduction），相繼式演算（ Sequent calculus）, Hauptsatz(cut elimination)等..
Theorem proving, automatic deduction/reasoning..
我相信做這些的很多人可能並不懂證明論，但是...引用F.Pfenning的話：
「Most search strategies employed by automated deduction systems are eitherdirectly based on or can be derived from the sequent calculus. .... Among the
backward searching procedures we findtableaux, connection methods, matrix
methods and some forms of resolution. Among the forward searching procedures
we find classicalresolutionand the inverse method..."
Programming language, type theory, formal verification...
間接影響Curry-Howard isomorphism，substructural type等；基於相繼式演算可以設計program logic的proof system；相繼式演算還能作為編譯器的中間語言[1]。。。
Artificial intelligence, database theory...?不太了解...
[1]Sequent calculus as a compiler intermediate language, Paul Downen, Luke Maurer
Zena M. Ariola and Simon Peyton Jones, ICFP 2016