Unification et élimination gaussienne

22

Quelqu'un connaît-il des références qui définissent précisément le lien entre l' algorithme d'unification et l'élimination gaussienne? Je suis particulièrement intéressé par la relation entre les substitutions triangulaires et les décompositions LU.

Wayne Snyder et Jean Gallier mentionnent cette analogie en passant dans leur article, Unification d'ordre supérieur revisité: ensembles complets de transformations .

reference-request lo.logic Neel Krishnaswami
la source
7
En tant que non-expert, je n'avais jamais entendu parler de la connexion. Une référence qui mentionne cette connexion serait un bon ajout à la question.
Tsuyoshi Ito
1
comme ils le disent dans l'article p2, c'est surtout une analogie, "qui dans le cas d'ordre supérieur tombe en panne". il existe une connexion ou une analogie démontrable entre la résolution et l'élimination gaussienne. assez proche?
vzn
4
Je suppose que vous le savez déjà: l'algorithme d'Euclide, l'élimination gaussienne, l'algorithme de Buchberger pour les bases de Grobner et l'achèvement de Knuth-Bendix sont censés former une séquence strictement croissante en termes de généralité et de méthode qu'ils utilisent. Si les cartes précises entre ces méthodes sont connues, peut-être pourriez-vous dériver la connexion ci-dessus?
Vijay D
@VijayD: Je ne le savais pas, en fait! Je sais ce que fait l'algorithme de Buchberger, mais je ne connais pas l'algorithme lui-même, ni rien du tout sur sa relation avec l'élimination guassienne ou l'achèvement de la base de connaissances.
Neel Krishnaswami

Réponses:

9

Je ne considère pas cela comme une réponse. J'abuse de la boîte de réponse pour imprimer un commentaire.

Il y a un sens strict dans lequel l'algorithme GCD d'Euclide, l'élimination gaussienne, l'algorithme de Buchberger et Knuth-Bendix forment une séquence stricte de généralisations et sont tous des exemples de ce qu'on appelle un algorithme de complétion . Il existe également une relation étroite entre ces algorithmes et la résolution en logique. Je ne connais pas de bonne référence pour cela mais j'ai vu le fait mentionné très souvent. Cela pourrait aider.

  1. Historique et caractéristiques de base de la procédure de paire critique / achèvement , Bruno Buchberger, 1987
  2. Systèmes canoniques de réduction en mathématiques symboliques , Franz Winkler. Lien Springer

Faites-moi savoir si vous trouvez de meilleures références.

Vijay D
la source