Raisonnement logique et démonstration automatique de théorèmes
Le raisonnement logique et la démonstration automatique de théorèmes concernent l'utilisation de la logique formelle pour représenter les connaissances et l'automatisation de la déduction, en tirant des conclusions qui découlent nécessairement d'un ensemble de prémisses.
Definition
La démonstration automatique de théorèmes est la dérivation automatisée permettant de déterminer si une formule logique découle d'un ensemble d'axiomes, généralement en manipulant les formules avec des règles d'inférence correctes jusqu'à ce que l'objectif soit atteint ou qu'une contradiction soit obtenue.
Scope
Ce sujet couvre le raisonnement en logique propositionnelle et du premier ordre, ainsi que les algorithmes qui l'automatisent : la vérification de la satisfiabilité basée sur les tables de vérité et DPLL pour la logique propositionnelle, l'unification et le principe de résolution pour la logique du premier ordre, le chaînage avant et arrière, et les fondements de la programmation logique. Il aborde la correction (soundness), la complétude (completeness) et la décidabilité des procédures d'inférence. Le raisonnement qui tolère l'incertitude ou les valeurs par défaut est traité dans les sujets connexes sur le raisonnement en présence d'incertitude et le raisonnement non monotone.
Core questions
- Que signifie pour une conclusion d'être impliquée par un ensemble de prémisses, et comment l'implication est-elle vérifiée mécaniquement ?
- Comment le principe de résolution, avec l'unification, fournit-il une règle d'inférence unique et complète pour la logique du premier ordre ?
- En quoi le chaînage avant et le chaînage arrière diffèrent-ils en tant que stratégies d'inférence ?
- Quelles sont les limites du raisonnement automatisé, étant donné que la validité du premier ordre n'est que semi-décidable ?
Key concepts
- logique propositionnelle et du premier ordre
- implication et validité
- unification
- résolution et réfutation
- DPLL et résolution de problèmes SAT
- chaînage avant et arrière
- clauses de Horn et programmation logique
- correction et complétude
Key theories
- Principe de résolution
- La résolution de Robinson est une règle d'inférence unique sur les clauses qui, combinée à l'unification, est complète par réfutation pour la logique du premier ordre : tout ensemble de clauses insatisfiable peut être démontré insatisfiable en dérivant la clause vide.
- DPLL et satisfiabilité propositionnelle
- La procédure de Davis-Putnam et son raffinement DPLL décident de la satisfiabilité propositionnelle par une division systématique des cas avec propagation unitaire et élimination des littéraux purs, constituant la base des solveurs SAT modernes.
- Programmation logique et chaînage arrière
- Restreindre la logique du premier ordre aux clauses de Horn et résoudre les objectifs en chaînage arrière conduit à la programmation logique, où le calcul est une recherche de preuve, offrant à la fois une méthode de raisonnement et un paradigme de programmation.
Clinical relevance
La démonstration automatique de théorèmes et la résolution de problèmes SAT/SMT sont utilisées dans la vérification matérielle et logicielle, l'analyse de programmes, la planification et les mathématiques, tandis que les langages de programmation logique tels que Prolog appliquent l'inférence par chaînage arrière aux bases de données, à l'analyse syntaxique et aux systèmes basés sur des règles.
History
Les premières procédures de preuve de Gilmore, Davis et Putnam (1960) ont automatisé le raisonnement propositionnel et quantificatif, et le principe de résolution de Robinson (1965) a unifié l'inférence du premier ordre en une seule règle. Les années 1970 ont vu la résolution être affinée pour donner naissance à la programmation logique et à Prolog ; la résolution de problèmes SAT et SMT est ensuite devenue une technologie pratique majeure.
Key figures
- John Alan Robinson
- Martin Davis
- Hilary Putnam
- Robert Kowalski
- Alan Robinson
Related topics
Seminal works
- robinson1965
- davis1960
- kowalski1979
Frequently asked questions
- Qu'est-ce que le principe de résolution ?
- La résolution est une règle d'inférence unique qui prend deux clauses contenant des littéraux complémentaires et produit une nouvelle clause combinant le reste. Appliquée de manière répétée avec l'unification, elle peut montrer qu'un ensemble de clauses du premier ordre est insatisfiable, ce qui constitue la base de la démonstration de théorèmes par réfutation.
- La démonstration automatique de théorèmes est-elle garantie de se terminer ?
- Pour la logique propositionnelle, la validité est décidable, de sorte que les procédures se terminent. Pour la logique du premier ordre complète, la validité n'est que semi-décidable : un prouveur complet confirmera finalement toute formule valide, mais peut s'exécuter indéfiniment sur une formule invalide, de sorte que la terminaison n'est pas garantie en général.