- The Hilbert calculi : many axioms, few inference rules. most of them has only one rules. the Modus Ponens, that is , P-> Q, P - Q. So most useful rules that invented latter in natural deduction, must be format in P-> Q style as axioms in this calculi.
- The natural deduction calculi : many rules, few axioms. Most famous one is that of Gentzen, which include premise over line, and conclusion under line. some of these rules include introductionand elimination rules for varias logic connective operator, such as /\ and \/.
- The sequent calculi : it is the final style we seen in " Logic For Computer ScienceFoundations ofAutomatic Theorem Proving", the famous system LK by Gentzen. I am not very sure if I has fully understand the difference between natural deduction and sequent calculi, it seems tha the later one is a enhanced version of the previous one, because I found structure rules in sequent calculi.
2008年10月10日星期五
relation of the 3 proof caculis in proof theory
there are three well know proof caculis:
订阅:
博文评论 (Atom)
没有评论:
发表评论