Estudia > Oferta formativa > Oferta d'assignatures > Detall de l'assignatura
Anar al contingut (clic a Intro)
UdG Home UdG Home
Tancar
Menú

Estudia a la UdG

Dades generals

Curs acadèmic:
2011
Descripció:
Sistemes de reescriptura. Demostració automàtica de teoremes. Programació funcional.
Crèdits:
5
Idioma principal de les classes:
Anglès
S’utilitza oralment la llengua anglesa en l'assignatura:
Indistintament (50%)
S’utilitzen documents en llengua anglesa:
Majoritàriament (75%)

Grups

Altres Competències

  • 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.

Continguts

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

Activitats

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

Bibliografia

  • 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

Avaluació i qualificació

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

Qualificació

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.

Observacions

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, ...

Assignatures recomanades

  • Eines lògiques i problemes combinatoris
  • Fonaments de la intel·ligència artificial

Escull quins tipus de galetes acceptes que el web de la Universitat de Girona pugui guardar en el teu navegador.

Les imprescindibles per facilitar la vostra connexió. No hi ha opció d'inhabilitar-les, atès que són les necessàries pel funcionament del lloc web.

Permeten recordar les vostres opcions (per exemple llengua o regió des de la qual accediu), per tal de proporcionar-vos serveis avançats.

Proporcionen informació estadística i permeten millorar els serveis. Utilitzem cookies de Google Analytics que podeu desactivar instal·lant-vos aquest plugin.

Per a oferir continguts publicitaris relacionats amb els interessos de l'usuari, bé directament, bé per mitjà de tercers (“adservers”). Cal activar-les si vols veure els vídeos de Youtube incrustats en el web de la Universitat de Girona.