Sadržaj:
Definicija - Što znači Unifikacija?
U računalnoj znanosti i logici objedinjavanje je algoritamski postupak koji se koristi u rješavanju jednadžbi koje uključuju simboličke izraze. Drugim riječima, zamjenom određenih varijabli podizražavanja drugim izrazima, objedinjavanje pokušava identificirati dva simbolička izraza. Ujedinjenje se koristi u tehnologiji automatiziranog zaključivanja, koja je i dalje jedno od glavnih područja primjene objedinjavanja.
Objedinjavanje se koristi u implementacijama kao što su:
- Programiranje jezičnog programiranja
- Logičko programiranje
- SMT solveri
- Analiza kriptografskog protokola
- Algoritmi prepisivanja termina
Ujedinjenje je jedna od osnovnih tehnika na kojoj se temelje metode automatiziranog odbitka.
Tehopedija objašnjava Unifikaciju
Izraz "ujedinjenje" i njegov pojam mogu se pripisati Johnu Alanu Robinsonu. On je upotrijebio ujedinjenje kao osnovnu operaciju svoga načela razlučivanja, a također je pokazao da objedinjujući pojmovi imaju najviše jedno opće sjedinjenje. Različiti okviri ujedinjenja razlikuju se na temelju izraza koji se javljaju u problemu ujedinjenja. Ujedinjenje prvog reda je ona u kojoj su varijable višeg reda (varijable koje predstavljaju funkcije) dopuštene u izrazima. Slobodno ujedinjenje ili sintaktičko ujedinjenje je rješenje u kojem je potrebno rješenje kako bi obje strane jednadžbe bile jednake.
Rješenje problema objedinjavanja prikazano je supstitucijom, što je preslikavanje simboličke vrijednosti svakoj varijabli koja je uključena u izraze problema. Drugim riječima, ključni cilj ujedinjenja je traženje supstitucije kako bi se objedinila dva dana termina. Očekuje se da će viši ujednačeni algoritam osigurati minimalan i potpun skup supstitucija (skup koji sadrži sva relevantna rješenja bez suvišnih članova) za zadani problem. Drugim riječima, objedinjavanje ne zanima samo rješivost određenog objedinjavanja ako je problem, već i ako je rješiva, u izračunavanju najopćenitijeg ujedinitelja.
Ujedinjenje se smatra jezgrom:
- Prolog implementacije
- Stručni sustavi temeljeni na umjetnoj inteligenciji
- Usklađivanje uzorka u funkcionalnim jezicima
- Određeni pristupi za raščlanjivanje
- Odvodne baze podataka
- Obrada prirodnog jezika
- Teorem dokazuje
- Unesite algoritme zaključivanja
