@ FII

Laborator: Terms. Logic Programming. Rewriting.

(2 puncte) Considerând dată o pereche Σ=(F, P) formată dintr-o mulțime de simboluri funcționale F și o mulțime de simboluri predicative P, definiți în Coq termenii de ordinul 1 ce pot fi construiți utilizând simbolurile din F (adică F-termenii).
(2 puncte) Definiți în Coq o funcție care primește la intrare la un termen t și o substituție σ și calculează termenul σ(t).
(4 puncte) Definiți în Coq noțiunea de unificator peste F-termenii de la exercițiul 1. Dați măcar două exemple de substituții care sunt unificatori pentru doi termeni și ilustrați acest lucru făcând calculele necesare.
(5 puncte) Calculați în Coq cel mai general unificator pentru doi termeni.