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

Praktikum 7 okt lükkub edasi!

Kell 14:00 praktikumi 7. oktoobril ei toimu (õppejõud koosolekul). Teeme edaspidi selle asemel täiendava praktikumi.

Hommikune loeng toimub.

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:

• 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.
• We will also have a look at:

• Solving propositonal formulae
• SMT methods

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.

You will probably want to run Vampire like this (try also vampire --help):

   vampire --mode casc --include ~/TPTP ~/TPTP/Problems/ALG/ALG150+1.p

where the --mode casc thing makes vampire try out many strategies, not just running one.

Gkc runs many strategies by default, unless you give it an extra strategy selection file as a command line arg.

The gkc method for finding included axioms (the first two are the TPTP suggestions provers mostly follow):

• try Axioms folder under the problem folder (notice you could set a sumbolic link there or just copy)
• try the TPTP environment variable, under which look for Axioms folder
• try the /opt/TPTP folder (assuming we have /opt/TPTP/Axioms/... there)

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.