University of Bamberg
open search form
You are here

Information Systems and Applied Computer Sciences

Chair for AI Systems Engineering (AISE)

  1.  University of bamberg
  2. Faculties
  3. Information Systems and Applied Computer Sciences
  4. Subject groups
  5. Applied Computer Science
  6. Chair for AI Systems Engineering (AISE)
  7. News
  8. Talk by Chad Brow (Czech Technical University in Prague): Formalization of Mathematics in Higher Order Set Theory (Wed, Nov 16, 14:15-15:45)

Talk by Chad Brow (Czech Technical University in Prague): Formalization of Mathematics in Higher Order Set Theory (Wed, Nov 16, 14:15-15:45)

Title: Formalization of Mathematics in Higher Order Set Theory

Speaker: Chad Brown (Czech Technical University in Prague)

Abstract: Church's simple type theory is a formulation of higher-order logic upon which many interactive theorem provers are based. A benefit of using Church's type theory is that for many theories that have no first-order finite axiomatization, there are corresponding theories that do have higher-order finite axiomatization. I will introduce Church's type theory and sketch a finite axiomatiation of a set theory in which one can formalize mathematics. I will also discuss the interplay be interactive theorem proving and automated theorem proving in this context.

When: Wed, Nov 16, 14:15-15:45

Where: Erba, Room  WE5/04.004