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

Responder a