On Monday, May 1, at 3:30 pm in Math Building 357, Dylan Jager-Kujawa will be giving a presentation on computer aided proofs titled Automated Propositional Logic Proofs using Gentzen Deduction Trees as part of an Honors Project. This talk is open to all faculty and students.
Abstract: In the mid 1930s, Gerhard Gentzen devised an algorithm to prove propositional logic theorems. Gentzen’s method is similar to previous algorithms, in that it attempts to search for counterexamples to disprove a theorem, however it differs in that it breaks propositions into a number of sequents, each containing assumptions and conclusions.
While this results in a somewhat more intuitive proof, it has the added benefit of being very well suited to implementation by a computer. The use of trees, as well as a well-defined set of permitted operations, makes implementation of this algorithm far more natural than those of Gentzen’s peers. (Flyer in PDF form)