démonstrateur automatique de théorème
- Domaine
-
- intelligence artificielle
- Dernière mise à jour
Définition :
Programme informatique utilisant une séquence de règles d'inférence élémentaires pour démontrer la véracité d'un théorème.
Notes :
Le démonstrateur automatique de théorème a ses limites. Il ne peut fonctionner que pour des problèmes de logique élémentaire et exige un temps de traitement très long.
Comme exemples de démonstrateurs automatiques de théorème, on peut mentionner : LCF-ML, GIPSY et Stanford Pascal Verifier.
Termes privilégiés :
- démonstrateur automatique de théorème n. m.
- démonstrateur automatisé de théorème n. m.
Traductions
-
anglais
Auteur : Office québécois de la langue française,Termes :
- automatic theorem prover
- ATP
- mechanical theorem prover
- automated theorem prover
-
catalan
Auteur : Universitat Autònoma de Barcelona,Terme :
- demostrador automàtic de teoremes n. m.
-
espagnol
Auteurs : Consejo Superior de Investigaciones Cientificas,
Colegio de México,Terme :
- demostrador automático de teoremas s. m.
-
portugais
Auteurs : Centro de Linguística da Universidade Nova de Lisboa,
Universidade de São Paulo,Note :
Subárea da inteligência artificial: representação do conhecimento por meio de Lógica.
Terme :
- provador automático de teorema s. m.