返回Google圖書搜尋

Démonstration automatique

其他書名	Refutation par superposition de clauses équationnelles
出版	Laboratoire Informatique Theorique et Programmation, 1982
URL	http://books.google.com.hk/books?id=i12VtgAACAAJ&hl=&source=gbs_api

註釋RAPPEL SUR LES SYSTEMES DE REECRITURE. INTRODUCTION DU FORMALISME (B) DE CLAUSES EQUATIONNELLES ET COMPARAISON DE L'UTILISATION DE L'OPERATION DE SUPERPOSITION DANS CE FORMALISME AVEC LA RESOLUTION ORDINAIRE. INTRODUCTION DE LA "LOCKING RESOLUTION" DE BOYER ET RAPPEL DES RESULTATS DE COMPLETUDE QUI Y SONT ATTACHES. CES NOTIONS ET RESULTATS SONT TRANSPOSES DANS LE FORMALISME (B). INTRODUCTION DE L'AXIOMATISATION TRADITIONNELLE DE L'EGALITE ET TRANSPOSITION DE CETTE AXIOMATISATION DANS LE FORMALISME (B). ON DEMONTRE QUE L'OPERATION DE SUPERPOSITION DANS (B) EST UNE RESTRICTION COMPLETE DE L'OPERATION D'HYPERPOSITION. CECI REVIENT A PROUVER LA COMPLETUDE D'UNE RESTRICTION DE L'OPERATION DE PARAMODULATION, CE QUI CONSTITUE UN RESULTAT ORIGINAL. INTRODUCTION DE L'OPERATION DE NORMALISATION DES CLAUSES