[logic-ml] JAIST Logic Seminar Series (Feb 26, 13:30-15:30)

[Nao Hirokawa]

皆様

２月２６日（火）に行われます、ウィーン工科大学 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.
-----------------------------------------------------------------------