Seminário remoto "Lógicos em Quarentena" 28/10/2020 (quarta-feira) 16:00h
16 views
Skip to first unread message
Bruno Lopes
Oct 26, 2020, 7:01:11 AM10/26/20
to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA, Sociedade Brasileira de Computação
Data: 28 de outubro de 2020 (quarta-feira)
Horário: 16:00h GMT-3
Apresentador: Profa. Daniele Nantes (DM/UnB)
Título: Nominal Equational Problems
Resumo: We consider nominal equational problems of the form \exists \vec{W} \forall \vec{Y} :P, where P consists of conjunctions and disjunctions of equations s\approx_\alpha t (read: ``s is \alpha-equivalent to t''), freshness constraints a# t (read: ``a is fresh for t'') and their negations s \not \approx_\alpha t and \neg(a# t), where a is an atom and s, t are nominal terms. In addition to existential and universally quantified variables, problems can also have free variables. We give a general definition of solution parametric on the algebra used to provide semantics to the problem, and a set of simplification rules that can be used to compute solutions in the nominal term algebra. For the latter, we define notions of solved form from which solutions can be easily extracted, and show that the simplification rules are sound, preserving and complete. With a particular strategy of application for the rules, the simplification process terminates, specifying an algorithm to solve nominal equational problems. In particular, the algorithm can be used to decide the validity of a first-order equational formula in the nominal term algebra.
Horário: 16:00h GMT-3
Apresentador: Profa. Daniele Nantes (DM/UnB)
Título: Nominal Equational Problems
Resumo: We consider nominal equational problems of the form \exists \vec{W} \forall \vec{Y} :P, where P consists of conjunctions and disjunctions of equations s\approx_\alpha t (read: ``s is \alpha-equivalent to t''), freshness constraints a# t (read: ``a is fresh for t'') and their negations s \not \approx_\alpha t and \neg(a# t), where a is an atom and s, t are nominal terms. In addition to existential and universally quantified variables, problems can also have free variables. We give a general definition of solution parametric on the algebra used to provide semantics to the problem, and a set of simplification rules that can be used to compute solutions in the nominal term algebra. For the latter, we define notions of solved form from which solutions can be easily extracted, and show that the simplification rules are sound, preserving and complete. With a particular strategy of application for the rules, the simplification process terminates, specifying an algorithm to solve nominal equational problems. In particular, the algorithm can be used to decide the validity of a first-order equational formula in the nominal term algebra.
A apresentação ocorrerá pelo Google Meet através do link público https://meet.google.com/row-kniu-dgm .
--
Bruno Lopes
Professor Adjunto
Instituto de Computação
Universidade Federal Fluminense
Reply all
Reply to author
Forward
0 new messages