M:K

[Ricardo Corin]

hola gente,
alguna gente me pregunto acerca de como hacer para resolver M:K.
Supongamos que es un predicado knows(M,K).
Tiene que ser verdad en los siguientes casos de test:
knows(m, [m,e]). (simple replay)
knows(hash(m), [m,e]). (constructor hash sobre m)
knows(encrypt(M,k), [encrypt(m,k)]). (unificacion de M y m)
knows(encrypt(e,k), [encrypt(k,k2),k2,e]). (desencriptacion de k
usando k2, y encriptacion de e con k)

A partir de un interleaving van a generar una query
knows(m1,K1),...., knows(mn,Kn) y ver si hay soliciones.

saludos!