44th TRS meeting Talks and abstracts
Jean-Pierre Jouannaud (Ecole Polytechnique), Well-founded Path Orderings for Operads.
Abstract: The definition of the Graph Path Ordering (GPO) on certain
graph expressions is inspired by that of the Recursive Path Ordering
(RPO), and enjoys all those properties that have made RPO popular, in
particular, well-foundedness, monotonicity, and totality on
variable-free terms.
We are indeed interested in a generalization of algebraic expressions
called operadic expressions, which are finite graphs each vertex of
which is labelled by a function symbol, the arity of which governs the
number of vertices it relates to in the graph. These graphs are seen
here as terms with sharing and back-arrows. Operadic expressions are
themselves multiplied (an associative operation) to form monomials,
which are in turn summed up (an associative commutative operation) to
form polynomials. Operadic expressions and their polynomials occur in
algebraic topology, and in various areas of computer science, notably
concurrency and type theory. Rewriting basic operadic expressions is
very much like rewriting algebraic expressions, while rewriting their
monomials and polynomials is very much like the Groebner basis
theory. GPO provides an initial building block for computing with
operadic expressions and their polynomials.
We shall discuss the many questions opened by this work in progress.
Stephan Merz (LORIA), Satisfiability Checking for Modal Logics via SMT Solving
Abstract: Modal logics extend classical propositional logic, and they are robustly decidable. Whereas most existing decision procedures for modal logics are based on tableau constructions, we propose a framework for obtaining decision procedures by adding instantiation rules to standard SAT and SMT solvers. Soundness, completeness, and termination of the procedures can be proved in a uniform and elementary way for the basic modal logic and some extensions.
(joint work with Carlos Areces and Pascal Fontaine)