Functions in Korppi Korppi


Log in!
May/27/2020 13:25

TIE0329 Automated reasoning, 4 ECTS, Lectured in English [home page]

Department of Mathematical Information Technology

The language used was temporarily changed. Personal information page allows you to save your language settings.
You cannot register for the course because the course has expired.
The registration deadline for this course passed 6.4.04 at 23:00.
Students will be registered according to their order of registration. Further information on queuing.

General information

Home page: http://www.mit.jyu.fi/antkaij/opetus/ap/2004/
Begins - ends: 2.3.04 - 16.4.04
Registration period: 1.9.03 at 0:00 - 6.4.04 at 23:00
Instructor(s): Antti-Juhani Kaijanaho (antti-juhani@kaijanaho.fi)
Credits: 4 ECTS cr.
Languages: language(s) of instruction: suomi; completion language(s): suomi
Registered: 35
Max participants: 60 (Due to the queuing method used for registration, you may still register for this course even though the number of participants exceeds the maximum.);
Organisations:Department of Mathematical Information Technology (MIT)
Current events:The course is lectured in English.
Contents:Normal forms, unification, resolution, tableaux, automated reasoning in equational theories, automated reasoning in higher-order logic.
Prerequisites:Automata and Formal Languages and either MAT223 Logiikka (2 cr) or FILA31 Logiikka 1. Functional Programming is recommended.
Modes of study:Lectures, exercises
Completion mode:Exam
Schedule:Lectures 20h on weeks 10-15, Tue 14-16 and Fri 10-12 in Ag Beeta
Literature:Fitting: First-Order Logic and Automated Theorem Proving (Second Edition). Wos et al.: Automated reasoning - introduction and applications. Robinson & Voronkov (eds.): Handbook of automated reasoning. Loveland: Automated theorem proving: a logical basis.

[Full information on teaching groups]

Lecture [group details and registration]

TIE329 Lectures (spring 2004) [group details and registration]; registered 35, maximum 40
reg.time: 1.9.2003 00:00 - 6.4.2004 23:00
 LocationWeekDayDateAtSupervisorFurther informationURI
1 - 10Ag Beeta, Ag Beeta, Ag Beeta, Ag Beeta, Ag Beeta, Ag Beeta, Ag Beeta, Ag Beeta, Ag Beeta, Ag C23410 - 16Tu, Fr2.3.2004 - 16.4.2004severalKaijanahoSyllabus. Introduction. ; Formal logic. Representation of logic as data in programs.; The sentential language. Truth tables.; Uniform notation, sentential case. Sentential tableaux.; Ground (dual) clauses. Davis-Putnam procedure.; Questions from the students. Skolemization.; Herbrand's theorem; Unification. Free-variable tableaux.; A Peek Beyond the Basics 10

Exercise group [group details and registration]

Demo [group details and registration]; registered 10, maximum 80
reg.time: 1.9.2003 00:00 - 6.4.2004 23:00
 LocationWeekDayDateAtSupervisorFurther informationURI
1 - 5Ag Alfa, Ag Alfa, Ag Alfa, Ag Alfa, Ag Alfa11 - 15Wed10.3.2004 - 7.4.2004severalKaijanaho1 2