Seminars

PROVAS E SINONÍMIA DE DERIVAÇÕES

Tiago Castro Alves
Universität Tübingen

08/06/2017, 15 h, sala 308 IC UFF

Procurarei apresentar alguns aspectos de idéias fundamentais à minha pesquisa de doutorado, cujo tema central é a chamada questão da identidade de provas. Duas das principais teses a respeito do tema - a saber, a tese da normalização, enunciada por Prawitz em caráter conjectural em 1971, e a da generalização, sugerida por Lambek em artigos publicados na mesma época - serão brevemente apresentadas, discutidas e comparadas. Com isso, espero poder oferecer algumas razões para esclarecer o pertencimento dessas teses a classificações distintas numa certa "taxonomia" de critérios para sinonímia de derivações, bem como expor alguns importantes aspectos conceituais mais gerais da questão abordados no trabalho que tenho desenvolvido.

The Automated-Reasoning Revolution: From Theory to Practice and Back (Moshe Y. Vardi)

Data: 15 de maio de 2017, segunda-feira, as 14:30h
Local: Auditório Padre Anchieta no prédio Cardeal Leme da PUC-Rio

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 Universidade de Rice e é editor da Communications of the ACM. Sua pesquisa é bastante extensa com trabalhos ligando lógica e computação.

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.