皆様
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)