Ser capaç d'estudiar propietats de sistemes de reescriptura, així com de fer demostracions elementals sobre aquestes. Ser capaç de reconèixer de quina manera un llenguatge/sistema està relacionat amb la reescriptura. Ser capaç de formalitzar i desenvolupar sistemes de reescriptura per a resoldre problemes reals mitjançant programació funcional.
1. Introducció i exemples 2. Reescriptura de primer ordre 2.1. Termes (contextos, ocurrències, subtermes, termes com a arbres, substitucions, matching, unificació) 2.2. Sistemes de reescriptura (relacions de reescriptura, formes normals, acabament, confluència local, confluència, monotonia, estabilitat sota substitucions) 2.3. Sistemes equacionals 2.4. La reescriptura com a mecanisme deductiu 3. Acabament 3.1. Ordres de reducció 4. Confluència 4.1. Lema de Newman 4.2. Parells crítics 5. Compleció 6. Deducció automàtica en lògica de primer ordre 7. Programació Funcional
Tipus d’activitat Hores amb professor Hores sense professor Total Elaboració individual de treballs 0 25,00 25,00 Sessió expositiva 25,00 25,00 50,00 Sessió pràctica 25,00 25,00 50,00 Total 50,00 75,00 125
Robinson, Alan Voronkov, Andrei (cop. 2001 ). Handbook of automated reasoning . Amsterdam [etc.]: Elsevier [etc.]. Catàleg Baader, Franz (1998 ). Term rewriting and all that . New York ; [etc.]: Cambridge UniversityPess. Catàleg Hindley, J. Roger (cop. 2008 ). Lambda-calculus and combinators, an introduction . New York: Cambridge University Press. Catàleg
Activitats d'avaluació: Descripció de l'activitat Avaluació de l'activitat % Classes de teoria Exercicis proposats 50 Classes de problemes Exercicis 25 Pràctiques de Laboratori 25
Hi haurà un nota de teoria, amb un pes del 50%, obtinguda mitjançant exercicis proposats durant el curs. La nota de laboratori (50%) s'obtindrà a partir de l'avaluació de les successives entregues dels exercicis a les classes de laboratori. També es podrà millorar la nota mitjançant l'estudi i presentació d'algun tema del curs.
Qualsevol tipus de computació pot veure's com a un procés de reescriptura. L'objectiu principal del curs és proporcionar una visió uniforme de diferents sistemes de reescriptura i algunes de les seves aplicacions. En particular es farà èmfasi en l'estudi de les propietats computacionals més interessants d'aquests sistemes, i en la seva aplicació en la demostració automàtica de teoremes i en llenguatges de programació funcionals, tractament de documents XML, ...