Formale Methoden und Deduktion Prof. Dr. J. Avenhaus

Inhalt

• Aktuelles
• Allgemeines
• Vorlesung
• Übungen
• Links

Aktuelles

• Auch nächstes Semester wird wieder ein Praktikum und ein (integriertes) Seminar angeboten. Die Vorbespechungen sind beide am Donnerstag, den 24. Juli 2003. Um 10:30 Uhr wird die Vorbesprechung des Praktikums beginnen - danach (circa 11:15 Uhr) dann die des Seminars.
• Für alle, die eine Prüfung ablegen müssen, um Kreditpunkte zu erhalten (angewandte Informatiker und Mathematiker und Andere) besteht die Möglichkeit dazu (mit den üblichen Zulassungskriterien) am Donnerstag den 7.8.2003. Bitte rechtzeitig vorher im Dekanat anmelden und bis zum 24.7.2003 im Sekretariat (34-417) die Prüfungszeit festlegen.

Allgemeines

• Semester: SS 2003
• Dozent: Prof. Dr. J. Avenhaus
• Ansprechpartner:
  • Tobias Wahl,
  • Tobias Schmidt-Samoa
• Jeder, der im FB Informatik eine Prüfung machen möchte, muss sich dazu rechtzeitig im Prüfungsamt im Dekanat anmelden. Das gilt natürlich auch bei Abschlussprüfungen zum Ende einer Vorlesung. Es wird dringend geraten, sich im www (oder direkt beim Prüfungsamt) nach den Anmeldungsfristen zu erkundigen und sich daran zu halten.

Vorlesung

• Die Vorlesung findet Dienstags um 10:00 Uhr und Donnerstag um 8:15 Uhr im Raum 46-110 statt.
• Literatur:
  • Bücher
    • J. Avenhaus, Reduktionssysteme, Springer, 1995
    • F. Baader and T. Nipkow, Term rewriting and all that, Cambridge 1998
    • L. Bachmair, Canonical Equational Proofs, Birkhäuser, 1991
    • E. Ohlebusch, Advanced Topics in Term Rewriting, Springer, 2002
  • Übersichtsartikel
    • N. Dershowitz an J.-P. Jouannaud, Rewrite systems, In J. van Leeuwen, Handbook of Theoretical Computer Science, volume B, chapter 6, pages 243-320, Elsevier 1990
    • N. Dershowitz and D. A. Plaisted, Rewriting In A. Robinson and A. Voronkov Handbook of Automated Reasoning, volume I, chapter 9, pages 535-610, Elsevier 2001
    • G. P. Huet and D. C. Oppen, Equations and rewriting rules: A survey, In R. V. Book, Formal Languages: Perspectives and Open Questions, pages 349-405, Academic Press 1980
    • J. W. Klop, Term rewriting systems, In S. Abramsky, Dov M. Gabbay and T. S. E. Maibaum, Handbook of Logic in Computer Science, volume 2, Background: Computational Structures, chapter 1, pages 1-116, Clarendon Press, Oxford, 1992
  • Zeitschriftenartikel
    • L. Bachmair and N. Dershowitw, Completion for rewriting modulo a congruence, In Theoretical Computer Science, 67:173-201, 1989
    • L. Bachmair and N. Dershowitz, Equational inference, canonical proofs and proof orderings, In Journal of the ACM, 41(2):236-276, 1994
    • L. Bachmair, N. Dershowitz an J. Hsiang, Orderings for equational proofs, In Proc. 1st Annual IEEE Symposium on Logic in Computer Science, 346-357, 1986
    • N. Dershowitz, Orderings for term rewriting systems, In Theoretical Computer Science 17:279-301, 1982
    • G. P. Huet, Confluent reductions: Abstract properties an applications to term rewriting systems, In Journal of the ACM, 27:797-821, 1980
    • J.-P. Jouannaud and H. Kirchner, Completion of a set of rules modulo a set of equations, IN SIAM Journal of Computation, 15:1155-1194, 1986
    • S. Kaplan, Conditional rewrite rules, In Theoretical Computer Science, 33:175-193, 1984
    • D. E. Knuth and P. B. Bendix, Simple word problems in universal algebras, In J. Leech, Computational Problems in Abstract Algebras, 263-297, Pergamon Press, 1970

• Vorlesungsfolien als Postscript: 2-17 18-33 34-49 50-57 58-73 74-89 90-109 110-125 126-137 138-153 154-165 166-193 194-213 214-233 234-249 250-269 270-285 286-309 310-329 330-356

  Vorlesungsfolien als GNU-gezipptes Postscript: 2-17 18-33 34-49 50-57 58-73 74-89 90-109 110-125 126-137 138-153 154-165 166-193 194-213 214-233 234-249 250-269 270-285 286-309 310-329 330-356

Übungen

• Es finden zwei Übungen statt: Dienstags um 13:45 Uhr im Raum 32-439 und Mittwochs um 10:00 Uhr in Raum 44-310.
• Übungsblätter als Postscript: 1 2 3 4 5 6 7 8 9 10 11
• Übungsblätter als GNU-gezipptes Postscript: 1 2 3 4 5 6 7 8 9 10 11

Impressum

AG Formale Methoden und Deduktion

Fachbereich Informatik

Technische Universität Kaiserslautern