Séminaire interuniversitaire de
logique mathématique
(3ème cycle FNRS)

Sauf mention contraire, les séminaires de l'après-midi ont lieu à l'ULB, Campus de la Plaine, au local 2NO906.

Programme de 1998-99

Résumés:

1. Dirk VAN HEULE: A tableau prover for the Partial Predicate Calculus.

   PPC presents a non-classical three-valued predicate calculus, where for a sequent (A₁,...,A_n |= B) the formulae at the left-hand side of the turnstile are considered to be TRUE, and the formula at the right-hand side of the turnstile is either TRUE or UNDEFINED. In this talk we extend this notion to sequents (A₁,..., A_n |= B₁, ... ,B_n), which mean that there are no counterexamples, i.e. models for which the expressions at the left-hand side of the turnstile are TRUE and the expressions at the right-hand side are FALSE. Note that the latter is a classical definition, but it gets a different interpretation in a three-valued logic.
   An automated tableau prover for the Partial Predicate Calculus (PPC) has been implemented and integrated in Isabelle. It is based on the LK object-logic but is extended to the three-valued logic of PPC. It provides three tactics: the tablo_tac which offers the opportunity to trace every step in the proof-process, the safe_tac based on depth-first search and the best_tac based on best-first search.
   A closed tableau is indicated by the fact that there are no more subgoals to prove, otherwise the subgoals define a counterexample for the expression.

2. Christian MICHAUX: Actions boreliennes de groupes polonais dénombrables.

   Une relation d'équivalence borelienne est dite dénombrable dès que toutes ses classes d'équivalences sont dénombrables. Un théorème de Feldman-Moore nous assure qu'une telle relation est toujours déterminée par l'action borelienne d'un groupe polonais dénombrable sur un espace polonais. Je donnerai un survol de la théorie descriptive des ensembles de telles relations et de certaines de leurs sous classes (hyperfinies, amenable,...). J'aborderai certains problèmes ouverts et montrerai que la conjecture de Vaught topologique (qui est une généralisation de la conjecture de Vaught pour L_omega1,omega) peut s'énoncer dans ce cadre.
   Cette séance aura lieu à Mons, au local 0A11

3. Maurice BOFFA: Un problème de décidabilité sur les algèbres de Kleene.

   Dans son livre "Regular Algebra and Finite Machines" (1971), J.H.Conway a montré que le système axiomatique engendré par les identités rationnelles (c'est-à-dire régulières, au sens de Kleene) pouvait se ramener à des identités associées aux groupes finis. Ce résultat reste le meilleur outil pour la recherche de systèmes complets d'identités rationnelles, mais il laisse certaines questions ouvertes comme par exemple celle de décider si une algèbre finie vérifie toutes les identités rationnelles.

4. Alexis BES: L'arithmétique de Skolem et ses extensions.

   Je proposerai un apercu des principaux resultats de definissabilite et de decidabilite lies a la theorie de la multiplication sur les entiers: Je parlerai en particulier de la methode des puissances generalisees de Feferman & Vaught qui permet d'obtenir des extensions decidables de (N,x), et des resultats sur les theories (N,x,R), ou R designe un fragment de la relation d'ordre.

5. Alexis BES: La théorie de la multiplication ordinale.

   Le résultat de Presburger sur la décidabilite de la theorie de (omega;+) a été étendu par Buchi qui a montré que Th(alpha;+) est décidable pour tout ordinal alpha. Par ailleurs on sait que Th(omega,x) est décidable; je montrerai que Th(alpha,x) est décidable ssi alpha < omega^omega, et présenterai des résultats de décidabilite pour des théories proches (du point de vue du pouvoir d'expression). Je rappellerai au début de l'exposé quelques éléments d'arithmétique ordinale, (ordinaux premiers, décomposition “unique”...) ainsi que les principaux résultats sur les théories ordinales.

6. Natacha PORTIER: Les algorithmes sur les corps: à quoi sert la dérivée ?

   On définit habituellement les algorithmes pour des mots booléens, c'est à dire des suites finies de 0 et de 1. Mais on peut les définir pour des mots sur un ensemble quelconque muni d'un nombre fini de fonctions et de relations (pour le cas des anneaux, voir le livre "Complexity and Real Computation", de L. Blum, F. Cucker, M. Shub et S. Smale, Springer-Verlag 1998, et pour le cas général, "les petits cailloux" de B. Poizat, ALEAS éditeur 1995). Je m'interesse plus particulièrement au cas des corps et des corps différentiels de caractéristique nulle. Les algorithmes qui utilisent la dérivée sont-ils plus puissants que ceux qui ne l'utilisent pas ?

7. Eric JALIGOT: Mauvais corps dans les groupes de rang de Morley fini.

   La question centrale dans le domaine des groupes de rang de Morley fini, connue sous le nom de conjecture de Cherlin-Zil'ber, est de savoir si un tel groupe simple est algébrique. Un programme de classification a été développé par Borovik, Cherlin et d'autres pour les groupes ordinaires, c'est-à-dire ceux qui, entre autres, n'interpretent pas de mauvais corps. Cette hypothèse technique simplifie de nombreux arguments puisqu'elle élimine certains groupes résolubles aux propriétés non algébriques, typiquement les groupes connexes, résolubles, non nilpotents et sans involutions. Comme les mauvais corps ont récemment été construits par Poizat, il convient de trouver de nouveaux arguments qui ne font pas intervenir ces corps, et je parlerai de certains succès récents dans cette direction.

8. Johann MAKOWSKI (Haifa, Zurich): Efficient Algorithms for Optimization and Enumeration Problems on Patchable Graphs.

   Graphs which occur as artefacts (VLSI, networks) created by humans are built stepwise (patched together) from simpler graphs and the history of this building process (patch tree) is usually known. Furthermore, the amount of information needed to do the patching is usually very small compared to the size of the graph. We shall introduce a way of measuring this information and call it the patch width pw(G) of a graph.

   We shall exhibit a class of such patching operations which allows us to use the patching history to make various decision, optimizitation and enumerations problems solvable in time f(k)O(n), where n is the size of the graph, and f(k) depends only on the patch width pw(G)=k, although these problems are NP-hard (#P hard) in general. Examples of small patch width are obtained in the case of graphs of tree width k, graphs of clique width k, P_4 sparse graphs, and other classes previously studied in the literature. We shall illustrate this method for solving SAT, #SAT, HAM and #HAM. Our method works for problems definable in Monadic Second Order Logic and uses a logical version of the Myhill-Nerode Theorem, the Feferman-Vaught Theorem, adapted to graphs. (Joint work with B. Courcelle and U. Rotics)

If you want to receive updated informations by email as soon as they are available, you may Register with us...
Archive des séminaires passés
Back to Mathematical Logic at the University of Mons-Hainaut
This page has been accessed times.