皆様

２月２６日（火）に行われます、ウィーン工科大学 Matthias Baaz 先生と インスブルック大学 Cezary Kaliszyk 先生の講演のお知らせです。 皆様、どうぞ奮ってご参加ください。

廣川　直 （北陸先端科学技術大学院大学 情報科学系）

----------------------------------------------------------------------- * JAIST Logic Seminar Series *

Date: Feb 26 (Tue), 2019, 13:30 - 15:30

Place: I-56 (Collaboration Room 7) on 5F of IS Building III at JAIST (Access: http://www.jaist.ac.jp/english/location/access.html)

-*- -*- -*- -*- -*- -*- -*- -*- -*-

Speaker: Matthias Baaz (Vienna University of Technology)

Title: On the benefit of unsound rules: Henkin quantifiers and beyond

Abstract: We give examples of analytic sequent calculi LK+ and LK++ that extend Gentzen's sequent calculus LK by unsound quantifier rules in such a way that i) derivations lead only to true sequents, ii) cut free proofs may be non-elementary shorter than cut free LK proofs. This research is based on properties of Hilbert's epsilon calculus and is part of efforts to complement Hilbert's stepwise concept of proof by useful global concepts. We use these ideas to provide analytic calculi for Henkin quantifiers demonstrate soundness, (cut free) completeness and cut elimination. Furthermore, we show, that in the case of quantifier macros such as Henkin quantifiers for a partial semantics global calculi are the only option to preserve analyticity.

-*- -*- -*- -*- -*- -*- -*- -*- -*-

Speaker: Cezary Kaliszyk (University of Innsbruck)

Title: Learning Theorem Proving from Scratch

Abstract: Machine learning can in some domains find algorithms that are better than human heuristics. In this talk we will look at various theorem proving problems and their heuristics, and see which of those can be replaces by machine learned strategies. Instead of typical brute-force search, we will consider Monte-Carlo simulations guided by reinforcement learning from previous proof attempts. Various predictors for estimating the usefulness of proof steps and the likelihood of closing the open tableaux branches will be compared. -----------------------------------------------------------------------