PessoALL: O seminário abaixo foi CANCELADO, a pedido do próprio palestrante.
Peço desculpas por qualquer inconveniente relacionado. Joao Marcos 2011/3/12 Joao Marcos: > Mais um seminário do LoLITA > (Group for Logic, Language, Information, Theory, and Applications) > desta vez em colaboração com o ForAll > (Formal Methods and Languages Research Laboratory) > da UFRN. > > Place: Auditório do CCET / UFRN > Date: Wed, 16-Mar-2011, 13:00-14:00 > > Title: > Algorithms for the compression of propositional resolution proofs > Speaker: > Bruno Woltzenlogel Paleo > https://sites.google.com/site/brunowp/ > > Abstract: > The resolution calculus is a minimalistic proof system widely used by > many automated theorem proving tools, such as sat-solvers, SMT-solvers > and first-order theorem provers. A proof (or refutation) explains why > a given formula is (or is not) a theorem. It is therefore a > certificate that the answer provided by a theorem proving tool is > indeed correct. > > For these reasons, among others, most modern theorem proving tools > store and output proofs. However, due to proof search heuristics and > optimizations, the obtained proofs are often rather redundant. > > In this talk, we will see some common kinds of redundancies in > propositional resolution proofs and algorithms to eliminate them. > > (Firstly, I will also introduce and explain the resolution calculus, > in order to allow students with no previous knowledge in this area to > follow the talk). > > > OBS: A palestra será apresentada em português. _______________________________________________ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
