View: session overviewtalk overviewside by side with other conferences

09:00 | Opening SPEAKER: Temur Kutsia |

09:15 | Extensible Symbolic System Analysis SPEAKER: Jose Meseguer ABSTRACT. Unification and narrowing are a key ingredient not only to solve equations modulo an equational theory, but also to perform symbolic system analysis. The key idea is that a concurrent system can be naturally specified as a rewrite theory (Sig,E,R), where (Sig,E) is an equational theory specifying the system's states as an algebraic data type, and R specifies the system's concurrent, and often non-deterministic, transitions. One can perform such symbolic analysis by describing sets of states as (the instances of) terms with logical variables, and using narrowing modulo E to symbolically perform transitions. Under reasonable conditions on the rewrite theory, this idea can be applied not only for complete reachability analysis, but also for temporal logic model checking. This approach is quite flexible but has some limitations. Could it be possible to make symbolic system analysis techniques more extensible and more widely applicable by simultaneously combining the powers of rewriting, narrowing, SMT solving and model checking? We give a progress report on current work aiming at such a unified symbolic approach. |

14:30 | On the Limits of Second-Order Unification SPEAKER: Jordi Levy ABSTRACT. Second-Order Unification is a problem that naturally arises when applying automated deduction techniques with variables denoting predicates. The problem is undecidable, but a considerable effort has been made in order to find decidable fragments, and understand the deep reasons of its complexity. Two variants of the problem, Bounded Second-Order Unification and Linear Second-Order Unification --where the use of bound variables in the instantiations is restricted--, have been extensively studied in the last two decades. In this paper we summarize some decidability/undecidability/complexity results, trying to focus on those that could be more interesting for a wider audience, and involving less technical details. |

15:30 | From Admissibility to a New Hierarchy of Unification Types SPEAKER: unknown ABSTRACT. Motivated by the study of admissible rules, a new hierarchy of ``exact'' unification types is introduced where a unifier is more general than another unifier if all identities unified by the first are unified by the second. A Ghilardi-style algebraic interpretation of this hierarchy is presented that uses exact algebras rather than projective algebras. Examples of equational classes distinguishing the two hierarchies are also provided. |