Fakultät für Informatik

TU München - Fakultät für Informatik
Software- and Systems Engineering Research Group


Vorlesung | Wintersemester 2012/2013
Applied Logic in Engineering
Dr. Maria Spichkova, Prof. Dr. Dr. h.c. Manfred Broy


Lecture: Applied Logic in Engineering

ECTS Credits:   6 (Module: IN3050)
4 (2 Lecture/2 Tutorial)
Lectures: Tuesday, 10:15 - 11:45, MI 00.13.009A "Multimedia" (Start: 16.10.2012)
Lecturer: Dr. Maria Spichkova
Tutorials: Thursday, 14:00 -15:30, MI 01.11.018 (Start: 25.10.2012)
Tutorial team: Dr. Maria Spichkova, Klaus Lochmann
Exam: Final written (open-book) exam at the end of the lecture period.
Date: 5.02.2013.
Time: 10:15
Room: MI 00.13.009A "Multimedia"

For questions regarding the lecture contact: Dr. Maria Spichkova.

David Parnas, a pioneer of software engineering, stated that a solid understanding of logic is essential for a software engineer. This statement is also true for any kind of engineering - from software engineering to the mechanical engineering.

We do not expect any previous knowledge and see this lecture as a "logic for everybody" who is studing an engineering subject and is interested in getting the knowledge about logic and its application areas. Estimated content of the lecture:

  • What is Logic?
    • History and application areas
    • "Dry formal methods" or "Sherlock Holmes deduction methods"?
    • Abstract representation
    • ProLog
    • Another way of thinking (in comparison with C, Java etc.)
    • Current industrial projects
  • Propositional logic
    • Syntax and semantics
    • Normal form transformation
    • Calculi
    • Natural deduction
    • Resolution
    • Binary decision diagrams
    • ProLog representation
  • First Order (predicate) logic
    • Syntax and semantics
    • Normal form transformation
    • Substitution
    • Calculi
    • Natural deduction
    • Resolution
    • ProLog representation
  • Other logics and where they are used
    • Datalogic (cf. also databases)
    • Description Logic: Entity-Relation Diagram, relation to the UML
    • Closed world assumption
    • HOL: Hypervisor Verification in VerisoftXT project (Microsoft)
  • Examples of application
    • Examples of formal specification + verification
    • Algebraic specification (cf. also the course "Grundlagen der Programm- und Systementwicklung")
    • Specification in Attempto Controlled English and current projects
    • Reasoning, problem of planning (AI, games etc.)

© Software & Systems Engineering Research Group
Sitemap |  Kontakt/Impressum
Letzte Änderung: 2013-01-30 15:10:28