Algoritmide ja andmestruktuuride erikursus

Course name: Advanced Algorithms and Data Structures in Automated Reasoning

Course code: ITI8590 Semester: fall 2019 Lecturer: Tanel Tammet Contact: tanel.tammet@ttu.ee, 6203457, ICT 426 Language: The default language of the course is English, but if all students understand Estonian, it will be in Estonian. Lectures per week: 1 lecture, 2 academic hours Practice work per week: 1 session, 2 academic hours Home work: additionally, mostly development and experimentation

Time and place

Ruumis 411.

Lectures: every Monday at 10:00-11:45 at ICT403

Practice sessions: Mondays at 14:00, but this may be changed during the first lectures in case students prefer some other suitable time.

Learning outcomes

In Estonian:

• teab mitmete erialgoritmide tööpõhimõtteid
• on suuteline rakendama neid algoritme erinevate ülesannete lahendamiseks
• teab mitmete andmestruktuuride tööpõhimõtteid ja on suuteline neid rakendama
• suudab analüüsida järjestikuste ja rekursiivsete algoritmide keerukust

Brief description of the course

The course focuses on the internals of the methods of automated reasoning:

• Introductory part:

• Solving propositonal formulae
• SMT methods

• The main bulk of the course: algorithms and data structures used for full first order (FOL) reasoners.
• The latter part will be extended to algorithms and data structures for extending standard FOL reasoners to the tasks of commonsense reasoning.

Course materials

Will be given during the course. Materials are either presentations for specific methods or scientific papers covering such methods.

• An introductory material to field is the set of course notes from Geoff Sutcliffe.

• A simpler introduction in Estonian book chapter pages 297-345 by Tanel Tammet.

• The second most important material is course notes by Stephan Schulz: this concerns implementation aspects.

• In case you want to see a highly theoretical intro to the field, check out Christoph Weidenbach's coursebook

Practice work

Will contain all of these:

• Writing problem converters
• Writing small, toy prover components
• Experimenting with automated reasoning systems on specific problem sets

Practice work 1

Get some provers running (at least two, but more is better!):

• Go check the current top provers for the First-order Theorems division of the latest casc competition. You may want to have a brief look at short system descriptions.

• Download and install at least Vampire (the overall top prover) and GKC (the new prover by T.Tammet, targeting large problems)

• Download and unpack TPTP problem set: here is the direct download link).

• Have a quick look at the TPTP technical manual

• Try to get the PyRes running: this is a pedagogical prover in Python by Stephan Schulz.

You may also run these on dijkstra like this:

ssh kasutajanimi@dijkstra.cs.ttu.ee

Practice work 2

Familiarize yourself with the provers:

• Run Vampire and GKC on some smaller problems in TPTP: start with initial problems from the PUZ domain (puzzles) and then the KRS domain (knowledge representation). Read the output and understand the basics.

• Encode some small problems from the Tammet book chapter or Sutcliffe material and run the provers on these. Read the output and undestand the basics.

Practice work 3

Do some excercises and exam style questions from the first chapters of the Sutcliffe tutorial (select yourself some from the excercizes and exam style questions)

Practice work 4

Build a script to run both Vampire and GKC on the TPTP KRS domain, considering only problems ending with +*.p like KRS119+1.p:

• Find if there are any provable problems Vampire fails on in 30 seconds, list these.

• Find if there are any provable problems GKC fails on in 30 seconds, list these.

This may be helpful: an example script for provers. It is *not* exactly the script you finally need, but you may get useful inspiration/ideas.