Raciocínio Lógico e Prova de Teoremas

O raciocínio lógico e a prova de teoremas dizem respeito ao uso da lógica formal para representar o conhecimento e à automação da dedução, derivando conclusões que necessariamente decorrem de um conjunto de premissas.

Definition

A prova de teoremas é a derivação automatizada de se uma fórmula lógica decorre de um conjunto de axiomas, tipicamente manipulando as fórmulas com regras de inferência corretas até que o objetivo seja derivado ou uma contradição seja alcançada.

Scope

Este tópico abrange o raciocínio em lógica proposicional e de primeira ordem e os algoritmos que o automatizam: verificação de satisfatibilidade baseada em tabelas de verdade e DPLL para lógica proposicional, unificação e o princípio da resolução para lógica de primeira ordem, encadeamento para frente e para trás, e os fundamentos da programação lógica. Aborda a correção, completude e decidibilidade dos procedimentos de inferência. O raciocínio que tolera incerteza ou padrões é tratado nos tópicos relacionados sobre raciocínio sob incerteza e raciocínio não monotônico.

Core questions

• O que significa para uma conclusão ser implicada por um conjunto de premissas, e como a implicação é verificada mecanicamente?
• Como o princípio da resolução, com unificação, fornece uma única regra de inferência completa para a lógica de primeira ordem?
• Como o encadeamento para frente e para trás diferem como estratégias de inferência?
• Quais são os limites do raciocínio automatizado, dado que a validade de primeira ordem é apenas semi-decidível?

Key concepts

• lógica proposicional e de primeira ordem
• implicação e validade
• unificação
• resolução e refutação
• DPLL e resolução SAT
• encadeamento para frente e para trás
• cláusulas de Horn e programação lógica
• correção e completude

Key theories

Princípio da resolução

A resolução de Robinson é uma única regra de inferência sobre cláusulas que, combinada com a unificação, é completa por refutação para a lógica de primeira ordem: qualquer conjunto insatisfatível de cláusulas pode ser demonstrado insatisfatível derivando a cláusula vazia.

DPLL e satisfatibilidade proposicional

O procedimento de Davis-Putnam e seu refinamento DPLL decidem a satisfatibilidade proposicional por divisão sistemática de casos com propagação unitária e eliminação de literais puros, formando a base dos modernos resolvedores SAT.

Programação lógica e encadeamento para trás

Restringir a lógica de primeira ordem a cláusulas de Horn e resolver objetivos para trás resulta na programação lógica, na qual a computação é uma busca por prova, fornecendo tanto um método de raciocínio quanto um paradigma de programação.

Clinical relevance

A prova automatizada de teoremas e a resolução SAT/SMT são utilizadas na verificação de hardware e software, análise de programas, planejamento e matemática, enquanto linguagens de programação lógica como Prolog aplicam inferência de encadeamento para trás a bancos de dados, análise sintática e sistemas baseados em regras.

History

Os primeiros procedimentos de prova de Gilmore, Davis e Putnam (1960) automatizaram o raciocínio proposicional e quantificacional, e o princípio da resolução de Robinson (1965) unificou a inferência de primeira ordem em uma única regra. A década de 1970 viu a resolução ser refinada na programação lógica e no Prolog; a resolução SAT e SMT posteriormente se tornou uma importante tecnologia prática.

Key figures

• John Alan Robinson
• Martin Davis
• Hilary Putnam
• Robert Kowalski
• Alan Robinson

Seminal works

• robinson1965
• davis1960
• kowalski1979

Frequently asked questions

O que é o princípio da resolução?

A resolução é uma única regra de inferência que pega duas cláusulas contendo literais complementares e produz uma nova cláusula combinando o restante. Aplicada repetidamente com unificação, ela pode mostrar que um conjunto de cláusulas de primeira ordem é insatisfatível, o que é a base para provar teoremas por refutação.

A prova automatizada de teoremas tem garantia de terminação?

Para a lógica proposicional, a validade é decidível, então os procedimentos terminam. Para a lógica de primeira ordem completa, a validade é apenas semi-decidível: um provador completo eventualmente confirmará qualquer fórmula válida, mas pode rodar indefinidamente em uma inválida, então a terminação não é garantida em geral.