Functions in Korppi Korppi


Log in!
Feb/20/2020 00:07

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@jyu.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.

[Limit information on study 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 informationURITapahtuman tiedot
1Ag Beeta10Tu2.3.200414:00-16:00KaijanahoSyllabus. Introduction. Tapahtuman tiedot
2Ag Beeta10Fr5.3.200410:00-12:00KaijanahoFormal logic. Representation of logic as data in programs.Tapahtuman tiedot
3Ag Beeta11Tu9.3.200414:00-16:00KaijanahoFormal logic.Tapahtuman tiedot
4Ag Beeta11Fr12.3.200410:00-12:00KaijanahoThe sentential language. Truth tables.Tapahtuman tiedot
5Ag Beeta12Tu16.3.200414:00-16:00KaijanahoUniform notation, sentential case. Sentential tableaux.Tapahtuman tiedot
6Ag Beeta12Fr19.3.200410:00-12:00KaijanahoGround (dual) clauses. Davis-Putnam procedure.Tapahtuman tiedot
7Ag Beeta13Tu23.3.200414:00-16:00KaijanahoQuestions from the students. Skolemization.Tapahtuman tiedot
8Ag Beeta14Tu30.3.200414:00-16:00KaijanahoHerbrand's theoremTapahtuman tiedot
9Ag Beeta14Fr2.4.200410:00-12:00KaijanahoUnification. Free-variable tableaux.Tapahtuman tiedot
10Ag C23416Fr16.4.200410:00-12:00KaijanahoA Peek Beyond the BasicsURITapahtuman tiedot

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 informationURITapahtuman tiedot
1Ag Alfa11Wed10.3.200414:00-16:00KaijanahoURITapahtuman tiedot
2Ag Alfa12Wed17.3.200414:00-16:00KaijanahoURITapahtuman tiedot
3Ag Alfa13Wed24.3.200414:00-16:00KaijanahoTapahtuman tiedot
4Ag Alfa14Wed31.3.200414:00-16:00KaijanahoTapahtuman tiedot
5Ag Alfa15Wed7.4.200414:00-16:00KaijanahoTapahtuman tiedot