Caros, No dia 15 de maio, segunda-feira, as 14:30h no auditório Padre Anchieta no prédio Cardeal Leme da PUC-Rio teremos apalestra do Projeto. Moshe Vardi.
Dentre os diversos prêmios que o Prof. Moshe Vardi obteve estão o ACM SIGACT Goedel Prize, ACM SIGMOD Codd Award, IBM Outstanding Innovation Awards e Blaise Pascal Medal. Mais detalhes sobre sua contribuição para a área de Ciência de Computação consulte http://www.cs.rice.edu/~vardi/. Atualmente o Prof. Vardi está na Univesridade de Rice e é editor da Communications of the ACM. Sua pesquisa é bastante extensa com trabalhos ligando lógica e computação. Segue abaixo o título e resumo da palestra, que visa a uma audiência bem ampla de pessoas ligadas a área de Ciência de Computação, Lógica e Matemática. Title and Abstract : The Automated-Reasoning Revolution: From Theory to Practice and Back Moshe Y. Vardi Rice University For the past 40 years, computer scientists generally believed that NP-complete problems are intractable. In particular, Boolean satisfiability (SAT), as a paradigmatic automated-reasoning problem, has been considered to be intractable. Over the past 20 years, however, there has been a quiet, but dramatic revolution and very large SAT instances are now being solved routinely as part of software and hardware design. In this talk, I will review this amazing development and show how automated reasoning is now an industrial reality. I will then describe how we can leverage SAT solving to accomplish other automated-reasoning tasks. Counting the number of satisfying truth assignments of a given Boolean formula or sampling such assignments uniformly at random are fundamental computational problems in computer science with applications in software testing, software synthesis, machine learning, personalized learning, and more. While the theory of these problems has been thoroughly investigated since the 1980s, approximation algorithms developed by theoreticians do not scale up to industrial-sized instances. Algorithms used by the industry offer better scalability but give up certain correctness guarantees to achieve scalability. We describe a novel approach, based on universal hashing and Satisfiability Modulo Theory, that scales to formulas with hundreds of thousands of variables without giving up correctness guarantees. Abraços, Bruno. -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para [email protected]. Para postar neste grupo, envie um e-mail para [email protected]. Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAFfvUVhvEsU-Y_iy1-C2dVsfrpzaq79gSiCTu%2BsuDR7hBuDbQg%40mail.gmail.com.
