Modules in Computational Logic at TU Wien
Keywords: propositional logic; first order logic; deduction;
proof theory; abduction and induction; knowledge representation
and reasoning; complexity theory; computer algebra.
The module offers a comprehensive introduction to Computational Logic
covering the main subareas as well as main methods and
techniques. After recalling basic notions from propositional and first
order logic, complexity theory and computer algebra, the areas of
equational reasoning, deduction, proof theory, abduction and
induction, non-monotonic reasoning, logic-based program development,
natural language processing and machine learning as well as logic and
connectionism are covered.
Courses in 2009/2010:
Winter Semester
Summer Semester
Keywords: unification; declarative, procedural, and
operational semantics; logic programming; constraint logic
programming; combinatorics and analysis of algorithms.
This module is concerned with the foundations of logic programming
and constraint logic programming. The basic computation mechanisms
of unification and SLD-resolution are introduced. The declarative
and the operational semantics of logic programs are given and
related to the procedural semantics. A logic programming language
is introduced as an example of a declarative programming language.
Logic programs with constraints are introduced and basic
computation mechanisms given. The module concludes with examples
of constraint logic programming languages. In addition basic
knowledge of combinatorics and analysis of algorithms is
taught.
After the successful completion of this module, students will have
acquired a profound understanding of the mathematical principles
of logic programming. Students will also have experience in using
logic programming languages and constraint logic programming
languages for problem solving.
Courses in 2009/2010:
Summer Semester
Keywords: higher order logics; lambda calculus; lambda
prolog; modal logics, epistemic logic; temporal logic;
mu-calculus; CTL*; schematic tableaux; model theory.
The aim of this module is to introduce basic concepts beyond
first-order predicate logics. In Computer Science many different
logics and deductive systems exist. First we introduce higher
order logic (HOL) as a framework for specifying syntactic and
deductive notions of different logics. HOL is used in several
interactive proof tools, like PVS and Isabelle. In addition,
specific families of logics aimed at different application areas
are introduced: logics of time and computation (modal logics,
temporal Logics), logics for reasoning about knowledge (epistemic
logic). Finally we introduce the mu-calculus which allows to
define recursive temporal properties and we present a tableau
based deduction calculus for the mu-calculus. The mu-calculus and
its deduction system can be used to define problem oriented
systems of modal operators and corresponding deduction
systems.
Courses in 2009/2010:
Winter Semester
Summer Semester
Keywords: Logic & computers, logic & other systems; logic & interfaces; logic & applications.
The module shall meet the demand for more practice-oriented
subjects in the curriculum. By means of selected examples it
shall give an insight to various issues of how logic can be used
in real world applications. The students shall be introduced to
how logic can be linked to computers (e.g. data structures, WAM,
distributed computation), to other systems (e.g. ODCB, Oracle,
Java, Interplay between Prolog and data bases) and to human
interfaces (e.g. ML, Java). The principle techniques shall be
supplemented by examples.
Courses in 2009/2010:
Winter Semester
Summer Semester
This module deals with the theoretical foundations of
computation and with practical realizations. On the theoretical side it
covers the theory of computability (computable functions, recursion
theory, degrees of unsolvability), complexity theory (NP-completeness,
the polynomial hierarchy NP-approximation), and different computing
paradigms like quantum computation. On the practical side the areas
functional programming and constraint logic programming are covered.
Courses:
- Complexity Theory (3 cr.)
- Theory of Computability (3 cr.)
- Quantum Computing (3 cr.)
- Advanced Functional Programming (3cr.)
- Constraint Logic Programming (3 cr.)
- Seminar in Theoretical Computer Science (3 cr.)
- Selected Topics in Computer Science 1 (1.5 cr.)
- Selected Topics in Computer Science 2 (3 cr.)
- Selected Topics in Computer Science 3 (3 cr.)
- Selected Topics in Computer Science 4 (3 cr.)
- Selected Topics in Computer Science 5 (3 cr.)
Realization in 2009/2010:
Winter Semester
Summer Semester
This module deepens the knowledge in important
traditional fields of mathematical logic like proof theory, model
theory, set theory, lambda-calculus (typed and untyped) and
combinatory logic.
Courses:
- Proof Theory (4.5 cr.)
- Lambda-Calculus (3 cr.)
- Model Theory (3 cr.)
- Epsilon-Calculus (3 cr.)
- Set Theory (3 cr.)
- Selected Topics in Mathematical Logic 1 (1.5 cr.)
- Selected Topics in Mathematical Logic 2 (3 cr.)
- Selected Topics in Mathematical Logic 3 (3 cr.)
- Selected Topics in Mathematical Logic 4 (3 cr.)
- Selected Topics in Mathematical Logic 5 (3 cr.)
Realization in 2009/2010:
Winter Semester
- Lambda Calculus (3 cr.), Matthias Baaz
(WS 108.030, German title: AKLOG: Lambda Kalkül)
- Modal logic and epistemic logic (3 cr.), Christian Fermüller
(WS 185.269, German title: Modallogik, Epistemische Logik)
- Seminar in Theoretical Computer Science (3 cr.), Reinhard Pichler
(WS 181.185, German title: Seminar aus theoretischer Informatik und Logik)
- Seminar in Theoretical Computer Science (3 cr.),
Gernot Salzer, Rudolf Freund
(WS 185.320, German title: Seminar aus Theoretischer Informatik)
- Seminar in logic (3 cr.), Alexander Leitsch
(WS 185.318, German title: Seminar aus Logik)
- Seminar in Theoretical Computer Science (3 cr.), Uwe Egly et al.
(WS/SS 184.067, German title: Seminar aus Theoretischer Informatik) (available also in Summer Semester)
- Seminar in logic (3 cr.), Uwe Egly et al.
(WS/SS 184.264, German title: Seminar aus Logik) (available also in Summer Semester)
Summer Semester
- Fuzzy Logic (3 cr.), Matthias Baaz
(SS 104.103, German title: Fuzzy Logik)
- Computability Theory (3 cr.), Alexander Leitsch
(SS 185.203, German title: Theorie der Berechenbarkeit)
- Computational Equational Logic (3 cr.), Bernhard Gramlich
(SS 185.298, German title: Computationale gleichungsbasierte Logik)
- Seminar in logic (3 cr.), Christian Fermüller
(SS 185.316, German title: Seminar aus Logik)
-
Tableau Systems for Modal Logics, Hans Tompits (SS 184.223, German title:
Tableausysteme in der Modallogik)
Note: This course is given
in German only. Please talk directly to the lecturer if you would like to
complete it!
The aim of this module is the extension of advanced mathematical
knowledge which may be useful in solving difficult problems in
computational logic. The mathematical areas included in this module are
algebra, symbolic computation, discrete methods and combinatorics and
others.
Courses:
- Algebra (7 cr.)
- Symbolic Computation (5 cr.)
- Selected Topics in Number Theory (3 cr.)
- Discrete Methods (7 cr.)
- Theory of Graphs (3 cr.)
- Combinatorics (3 cr.)
- Topology (7 cr.)
- Mathematical Seminar (3 cr.)
No Realization in 2009/2010.
This module contains several areas where methods of logic are applied
in computer science. These areas are theory of data bases, deductive
data bases, web data extraction and integration, data and
knowledge-bases systems.
Courses:
- Computer Aided Verification (3 cr.)
- Theory of Data Bases (3 cr.)
- Deductive Data Bases (3 cr.)
- Web Data Extraction and Integration (3 cr.)
- Data and Knowledge-Based Systems. (4.5 cr.)
- Selected Topics in Computer Science 1 (1.5 cr.)
- Selected Topics in Computer Science 2 (3 cr.)
- Selected Topics in Computer Science 3 (3 cr.)
- Selected Topics in Computer Science 4 (3 cr.)
- Selected Topics in Computer Science 5 (3 cr.)
Realization in 2009/2010:
Winter Semester
- Knowledge Management VO (3 cr.), Jürgen Dorn
(WS 188.483, German title: Knowledge Management)
- Knowledge Management UE (3 cr.), Jürgen Dorn
(WS 188.486, German title: Knowledge Management)
- Machine Learning (3 cr.), Nysret Musliu
(WS 181.191)
- Cryptography (3 cr.), Uwe Egly
(WS 184.189, German title: Kryptographie)
- Deductive Databases (3 cr.), Stefan Woltran
(WS 184.247, German title: Deduktive Datenbanken)
- Web data extraction and integration (3 cr.), Robert Baumgartner
(WS 181.130, German title: Web Datenextraktion und -integration)
Summer Semester
- Database Theory (3 cr.), Georg Gottlob
(SS 181.140, German title: Datenbanktheorie (Neuer Studienplan))
- Applied Web Data Extraction and Integration (3 cr.), Robert Baumgartner
(SS 181.189)
- Advanced Database Systems (3 cr.), Reinhard Pichler
(SS 181.198)
- Problem Solving and Search in Artificial Intelligence (3 cr.), Nysret Musliu
(SS 181.190)
- Formal Verification of Software (6 cr.), Gernot Salzer
(SS 185.292, German title: Formale Verifikation von Software)
-
Seminar in Artificial Intelligence (3 cr.), Nysret Musliu
(SS 181.034, German title: Seminar aus Artificial Intelligence)
-
Reasoning about actions and change (3 cr.), Chitta Baral (SS 195.008)
This module presents several inference principles
in more detail. These principles are term rewriting, unification
theory, nonmonotonic reasoning, probabilistic reasoning and automated
deduction in nonclassical logics. Moreover various nonclassical logics
are introduced and their potential in modelling knowledge and reasoning
is investigated.
Courses:
- Term Rewriting (3 cr.)
- Unification Theory (1.5 cr.)
- Nonmonotonic Reasoning (3 cr.)
- Probabilistic Reasoning (3 cr.)
- Automated Deduction in Nonclassical Logics (3 cr.)
- Modal Logic and Epistemic Logic (3 cr.)
- Many-Valued Logics and Fuzzy Logic (3 cr.)
- Selected Topics in Mathematical Logic 1 (1.5 cr.)
- Selected Topics in Mathematical Logic 2 (3 cr.)
- Selected Topics in Mathematical Logic 3 (3 cr.)
- Selected Topics in Mathematical Logic 4 (3 cr.)
- Selected Topics in Mathematical Logic 5 (3 cr.)
Realization in 2009/2010:
Winter Semester
- Proof Theory 1 (3 cr.), Matthias Baaz
(WS 118.131, German title: AKLOG. Beweistheorie 1)
- Term Rewriting (3 cr.), Bernhard Gramlich
(WS 185.224, German title: Termersetzungssysteme)
- Seminar in Theoretical Computer Science (3 cr.),
Gernot Salzer, Rudolf Freund
(SS 185.320, German title: Seminar aus Theoretischer Informatik)
- Seminar in Theoretical Computer Science (3 cr.), Uwe Egly et al.
(WS/SS 184.067, German title: Seminar aus Theoretischer Informatik) (available also in Summer Semester)
- Seminar in logic (3 cr.), Alexander Leitsch
(WS 185.318, German title: Seminar aus Logik)
- Seminar in logic (3 cr.), Uwe Egly et al.
(WS/SS 184.264, German title: Seminar aus Logik) (available also in Summer Semester)
- Nonmonotonic Reasoning (3 cr.), Hans Tompits
(WS 184.188, German title: Nichtmonotones Schließen)
Summer Semester
- Proof Theory 2 (3 cr.), Matthias Baaz
(SS 118.211, German title: AKLOG. Beweistheorie 2)
- Automated Deduction (5 cr.), Alexander Leitsch
(SS 185.247, German title: Automatisches Beweisen)
- Seminar in logic (3 cr.), Christian Fermüller
(SS 185.316, German title: Seminar aus Logik)
-
Tableau Systems for Modal Logics, Hans Tompits (SS 184.223, German title:
Tableausysteme in der Modallogik)
-
Automated theorem proving in non-classical logics, Uwe Egly (SS 184.084, German title: Automatisches Beweisen in nichtklassische Logiken)
-
SAT Solving, Uwe Egly (SS 184.090, German title: SAT Solving und Erweiterungen)
Realization in 2009/2010:
Winter Semester
Summer Semester
For information on MSc Thesis, please contact Alexander Leitsch.
Further information
Other links for EMCL students at TUW:
List of modules and courses
Studying at TUW
Thesis and Graduation
General Information and Links
FAQs
