Lógica, Provas e Algoritmos

[ Próxima Página | Página Anterior | Página Principal ]


Peter Clote: Proof Length for Propositional Logic Systems

Duas noções intimamente relacionadas de complexidade de prova têm motivado a maioria dos trabalhos recentes na interface entre Ciência da Computação e Lógica Matemática. Uma delas gira em torno da questão do comprimento de uma prova, e a outra trata da complexidade de passos de inferência dentro de uma prova. Sabe-se muito bem NP=co-NP se e somente se todas as tautologias proposicionais têm provas curtas. Mas as conecções entre comprimento de provas e teoria da complexidade vai muito mais além. Limites inferiores em circuitos são intimamente ligados aos limites de comprimento de prova em sistemas formais restritos, e avanços em uma das frentes frequentemente leva a progressos na outra. Restringindo a complexidade de passos de inferência dentro de uma prova, pode-se obter um fragmento da Aritmética de Peano chamado de Aritmética Cotada (Bounded Arithmetic), que define exatamente os predicados na hierarquia polinomial. Trabalhos recentes e bastante promissores têm mostrado que se certas teorias formais de aritmética cotada podem provar limites inferiores em teoria da complexidade, então os sistemas criptógraficos correspondentes não poderão ser seguros.

A programação da visita do Prof Peter Clote incluiu a apresentação das seguintes palestras:

Quarta-Feira 11 de Setembro, 09:00-11:15 (com pausa de 15min)
Tutorial on Proof Length for Propositional Logic Systems

Quinta-Feira 12 de Setembro, 09:00-10:00
Evolution as a Computational Engine

Quinta-Feira 12 de Setembro, 14:30-15:30
Cutting Planes, Connectivity and Threshold Logic

Segunda-Feira 16 de Setembro, 10:00-11:00
Lower Bounds for Cutting Planes and Threshold Logic

Segunda-Feira 16 de Setembro, 16:00-17:00
Function Algebras and Complexity Classes

Entre os tópicos apresentados no Tutorial apresentado pelo Prof Peter Clote destacam-se:

  • Apresentação dos resultados clássicos sobre propositional proof systems (Cook-Reckhow): a existência de um sistema de prova proposicional limitado polinomialmente é equivalente à questão NP=co-NP.

  • Exemplos de sistemas de prova proposicionais.

  • Apresentação do teorema de Cook-Urquhart sobre o número de nós interiores de um tableau semântico mínimo para uma fórmula proposicional.

  • Completude do método da resolução, e apresentação de uma generalização do método para permitir múltiplos cuts, o que leva naturalmente ao método de refutação de fórmulas na forma normal conjuntiva chamado de cutting planes (CP), e desenvolvido por W. Cook et al.

  • Apresentação do teorema de Reckhow (tese de doutorado) que estabelece que todos os sistemas (axiomáticos) de Frege são polinomialmente equivalentes.

  • Apresentação do teorema de Haken (1985) que diz que existe uma constante c>1 tal que toda refutação por resolução das tautologias do tipo pigeonhole principle com n variáveis tem pelo menos 2^{c*n} cláusulas.

  • Apresentação do teorema de Beame, Impagliazzo, Pitassi, Krajícek, Pudlák e Woods, sobre o comprimento de provas em sistemas de Frege.