Pretende-se obter novos resultados para fragmentos da lógica de predicados de primeira ordem, cujos modelos são palavras finitas e inifinitas. O projeto visa questões fundamentais motivadas por considerações práticas para a validação de software e circuitos. Desde o trabalho pioneiro de Büchi, Elgot e Trakthenbrot, as ligações entrem os mecanismos de descrição lógica e a teoria de autómatos é a principal ferramenta para a solução de tais problemas. Trabalho preliminar importante é devido ao responsável português, que foi o primeiro a considerar o problema da separação. O colaborador proposto, Manfred Kufleitner, estudou intensivamente fragmentos da lógica de primeira ordem. Esperamos conseguir combinar as ideias e métodos de cada parceiro para aprofundar o conhecimento em ambas as áreas. Pretende-se ainda estender a colaboração de ambos os lados a Thomas Place e Marc Zeitoun (Bordéus), investigadores que recentemente obtiveram sucessos notáveis na solução de problemas de separação.

Observações. Este projeto é coordenado com outro projeto bilateral, constituindo uma rede de cooperação envolvendo três países (Alemanha, França e Portugal). O financiamento indicado é o valor atribuído para o primeiro ano.