Abstract FR:

Presentation d'un nouvel algorithme de deduction associe au calcul propositionnel: l'evaluation semantique, obtenu en associant une propriete de coupure originale a la procedure de davis et putnam. D'une part les performances de l'algorithme presente se sont averees tres bonnes, et d'autre part il a ete possible de comparer formellement son efficacite avec celle de la sl-resolution de kowalski et kuehner