[logic-ml] JAIST Logic Seminar Series (Prof. Middeldorp & Prof. Chen): July 12 (Tue) 14:00, I-56

[Nao Hirokawa]

皆様

JAIST Logic Seminar Series のセミナー開催のお知らせを致します。
Ren-June Wang 教授の講演会に続きまして、7月12日(火) に
Middeldorp 教授と Chen 教授の講演会を開催致します。
皆様のご参加をお待ち申し上げます。

廣川 直 (JAIST)


===========================================================================
                      JAIST Logic Seminar Series
===========================================================================

Date:    July 12 (Tue) 14:00-16:45
Place:   Collaboration Room 7 (I-56), JAIST
Access:  http://www.jaist.ac.jp/english/location/access.html


                        -*-*- first talk -*-*-

Prof. Aart Middeldorp  (University of Innsbruck)

FORT 0.2: Confluence Properties on Open Terms in the First-Order
Theory of Rewriting

Abstract:
The first-order theory of rewriting is decidable for finite
left-linear right-ground rewrite systems. The decision procedure for
this theory is based on tree automata techniques and implemented in
FORT. FORT offers the possibility to synthesize rewrite systems that
satisfy properties that are expressible in the first-order theory of
rewriting.

Tree automata operate on ground terms. Consequently, variables in
formulas range over ground terms and hence the properties that FORT is
able to decide are restricted to ground terms. Whereas for termination
and normalization this makes no difference, for other properties it
does, even for left-linear right-ground rewrite systems. This raises
the question how one can use FORT to decide properties on open
terms. We show that for properties related to confluence it suffices
to add one or two fresh constants. We furthermore provide sufficient
conditions which obviate the need for additional constants. These
results have been implemented in FORT 0.2.

In the talk, which is based on joint work with Franziska Rapp, I will
explain the decision and synthesis algorithms implemented in FORT,
before discussing the new results for deciding properties on open
terms. The talk is concluded with a comparison with AGCP, a tool
developed by Aoto and Toyama for checking ground-confluence of
many-sorted rewrite systems.


                       -*-*- second talk -*-*-

Prof. Yijia Chen  (Fudan University, Shanghai)

Random Graphs, First-Order Logic, and AC^0 Circuits

Abstract:
First-order logic (FO) has very limited expressive power. One of the
best-known examples is its 0-1 law on random graphs. Among others, it
implies that FO cannot express PARITY. However, once the graphs are
ordered, the 0-1 law completely breaks down. Thus, to prove FO cannot
define PARITY on ordered graphs, one uses the remarkable machinery of
Hastad's Switching Lemma on AC^0 circuits.

In 2008, Rossman proved that the k-clique problem cannot be defined by
FO using only k/4 variables, resolving a long-standing open problem in
finite model theory and complexity theory. His proof is built on a
brilliant application of Hastad's Switching Lemma on ordered random
graphs.

In the talk, I will explain our recent work extending Rossman's result
to the so-called planted clique conjecture. Among others, it shows
that any super-constant clique cannot be characterized by FO, even in
case that the given ordered graphs have a huge planted clique.

This is joint work with Joerg Flum (Freiburg)