Quels types de problèmes mathématiques peuvent être résolus par les prouveurs de théorèmes automatisés?

Puis-je prouver les énoncés suivants en utilisant les prouveurs de théorèmes automatisés disponibles?

. $(a+b)^2=a^2+b^2+2ab$
Si , alors . $11 \mid 2a-3b$ $11 \mid 7a-5b$
Si , alors . $ax^2+bx+c=0$ $x=\frac{-b\pm\sqrt{b^2-4ac} }{2a}$
Si est pair alors est pair. $a$ $4a$

etc!

Je pose cette question parce que je viens de trouver l'application des prouveurs de théorèmes automatisés pour prouver des théorèmes en logique.

automated-theorem-proving Math-fort
la source

Vous pouvez certainement prouver tout cela (sauf peut-être 3, ce qui est faux comme écrit) en utilisant tous les assistants de preuve standard, bien que ce ne soit probablement pas automatique.

Yuval Filmus

@YuvalFilmus. Merci! Alors, quel type de problèmes peut être résolu automatiquement?

Math-fort

Vous pouvez simplifier les expressions automatiquement, bien qu'il s'agisse d'un service fourni par Computer Algebra Systems. Je ne pense pas que les assistants de preuve modernes puissent automatiquement prouver quoi que ce soit de substantiel, mais il vaut mieux demander aux experts.

Yuval Filmus

@YuvalFilmus Je pense que ce que vous dites est souvent vrai, en ce sens que ce n'est que lorsqu'une méthode de preuve automatisée donne des résultats intéressants que nous sommes prêts à l'appeler une partie d'un CAS ...

Lézard discret

"(a + b) ^ 2 == a ^ 2 + b ^ 2 + 2ab" sur WolframAlpha

Nat

Réponses:

La plupart de vos déclarations sont des algèbres élémentaires, elles peuvent donc être prouvées automatiquement par un système d'algèbre informatique (CAS), comme Maple ou Mathematica.

(Si vous êtes intéressé par les mathématiques derrière CAS, je peux recommander le livre Modern Computer Algebra de Joachim von zur Gathen et Jürgen Gerhard, un beau livre, considéré comme la `` bible '' du domaine)

La démonstration automatisée de théorèmes a tendance à être principalement un cas de recherche heuristique sur une structure qui représente des preuves, si la preuve n'est pas l'un des rares cas pour lesquels il existe un algorithme qui peut le résoudre de manière concluante. Étant donné que ces déclarations ne sont pas très compliquées, il est probable qu'un prouveur automatisé puisse «trouver» une preuve.

Cependant, je pense qu'il est intéressant d'en dire un peu plus sur les énoncés pour lesquels il existe de bons algorithmes:

L'énoncé 3 concerne (un cas très simple) les racines d'un (système) d'équations polynomiales et peut être résolu en trouvant une base de Gröbner avec l'algorithme de Buchberger. La base de Gröbner et l'algorithme de Buchberger pour en trouver un sont de très bons outils pour la démonstration automatisée de théorèmes. Par exemple, nous pouvons même prouver automatiquement des théorèmes élémentaires en géométrie en transformant automatiquement le problème en trouvant une racine d'une équation polynomiale de manière intelligente!

Une autre classe intéressante de théorèmes sont les déclarations exprimables en arithmétique Presburger sans quantificateur (en particulier, cette arithmétique est sans multiplication, donc cela ne s'applique pas à vos déclarations), car il existe un algorithme pour résoudre toutes ces déclarations, même si l'algorithme est un peu lent.

Lézard discret
la source