Dis-unification (datavetenskap)

Dis-unification , inom datavetenskap och logik , är en algoritmisk process för att lösa olikheter mellan symboliska uttryck .

Publikationer om upplösning

Alain Colmerauer (1984). "Ekvationer och inequationer på ändliga och oändliga träd". I ICOT (red.). Proc. Int. Konf. om femte generationens datorsystem . s. 85–99.
Hubert Comon (1986). "Tillräcklig fullständighet, system för omskrivning av termer och "Anti-unifiering" " . Proc. 8:e internationella konferensen om automatiskt avdrag . LNCS . Vol. 230. Springer. s. 128–140. "Anti-Uniification" syftar här på inekvationslösning, en namngivning som numera har blivit ganska ovanlig, jfr. Antiförening (datavetenskap) .
Claude Kirchner; Pierre Lescanne (1987). "Lösa diskvationer". Proc. LICS . s. 347–352.
Claude Kirchner och Pierre Lescanne (1987). Lösa disekvationer (Forskningsrapport). INRIA.
Hubert Comon (1988). Enande och disunification: Théorie et applications (PDF) (Ph.D.). INP de Grenoble.
Hubert Comon; Pierre Lescanne (mars–april 1989). "Ekvationella problem och disunification" . J. Symb. Comput. 7 (3–4): 371–425. doi : 10.1016/S0747-7171(89)80017-3 .
Comon, Hubert (1990). "Ekvationsformler i ordningssorterade algebror". Proc. ICALP . Comon visar att första ordningens logikteorin om jämlikhet och sorters medlemskap är avgörbar, det vill säga varje första ordningens logikformel byggd av godtyckliga funktionssymboler, "=" och "∈", men inga andra predikat, kan effektivt bevisas eller motbevisat. Med den logiska negationen (¬) kan icke-likhet (≠) uttryckas i formler, men ordningsrelationer (<) kan inte. Som en ansökan bevisar han tillräcklig fullständighet av termomskrivningssystem .
Hubert Comon (1991). "Disunification: A Survey" . I Jean-Louis Lassez; Gordon Plotkin (red.). Computational Logic — Essays in Honor of Alan Robinson . MIT Press. s. 322–359.
Hubert Comon (1993). "Fullständiga axiomatiseringar av vissa kvottermalgebras" (PDF) . Proc. 18:e Int. Coll. om automater, språk och programmering . LNCS. Vol. 510. Springer. s. 148–164 . Hämtad 29 juni 2013 .

Se även

Enande (datavetenskap) : lösa ekvationer mellan symboliska uttryck
Constraint logic programmering : införlivande av lösningsalgoritmer för särskilda klasser av ojämlikheter (och andra relationer) i Prolog
Begränsningsprogrammering : lösa algoritmer för särskilda klasser av ojämlikheter
Simplex algoritm : lösande algoritm för linjära ekvationer
Inequation : typer av inekvationer i matematik i allmänhet, inklusive ett kort avsnitt om att lösa
Ekvationslösning : hur man löser ekvationer i matematik