Colloquium 05/01: Dylan Jager-Kujawa on Automated Propositional Logic Proofs using Gentzen Deduction Trees

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)

 

 

 

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s