16-Mar-2011, 13:00-14:00
Auditório do CCET / UFRN Speaker: Bruno Woltzenlogel Paleo (https://sites.google.com/site/brunowp/)Seminário do LoLITA (Group for Logic, Language, Information, Theory, and Applications) em colaboração com o ForAll (Formal Methods and Languages Research Laboratory) da UFRN.
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.
