Mathematics is built on a formal system, including logic and the axioms of set theory. The study of the foundations of mathematics focuses on this formal system and possible alternative.
Algebraic logic offers algebraic descriptions of models appropriate for the study of various logics. The classical example is the equivalence of propositional calculus and Boolean algebras.
We are interested in residuated lattices (which include Boolean algebras, Heyting algebras and MV-algebras, for instance) and the corresponding logics. We also study decidability and the properties of proofs in substructural logics, i.e., logics that lack one of the usual structural rules.
Automated deduction is a field of artificial intelligence focused on rigorous, computer assisted proofs of mathematical theorems. Automated deduction can provide early insights into increasingly more technical areas of mathematics and also establish original, state-of-the-art theorems. While some human guidance is usually necessary to obtain complicated proofs by "automated" deduction, the proofs can then be routinely checked for correctness.
We are mostly using automated deduction in the area of nonassociative mathematics. Many proofs we obtained were humanized for publication in standard mathematical research journals. Other proofs are too long (tens of thousands of steps) but they nevertheless impact the field. Furthermore, feedback from working mathematicians helps researchers in automated deduction and leads to software improvements.
Go to the graduate admission application to submit your information. For information on admission requirements, visit the graduate academic programs page and locate your program of interest.
