Teadmispõhise tarkvaraarenduse meetodid / Methods of Knowledge Based Software Development 2017

Course code: ITI8600 (Ainekaart eesti keeles ITI8600)

Language: The default language of the course is English, but if all students understand Estonian, it will be in Estonian.

Lecturers:

• Tanel Tammet, tanel.tammet@ttu.ee, 6203457, TTÜ ICT-426 (handles ÕIS registrations)
• Juhan Ernits, juhan.ernits@ttu.ee, 6202326, TTÜ ICT-428
• Sven Nõmm, sven.nomm@ttu.ee, TTÜ ICT-424

Lab assistant:

• Priit Järv, priit.jarv1@ttu.ee

Past editions

2015, 2016

Time, place, result

• Lectures: Fridays 8:00-9:30, CYB-Veenus
• Labs: Fridays 14:00-15:30, ICT-121

Exam

• 5.01.2018
• 19.01.2018
• 22.01.2018

Grading

The final grade will be based on 40% of points from homework assignments and 60% of the result of an exam.

There will be four homework assignments, one for each block. Assignments will give up to 10 points each. In order to successfully pass the course, at least three homeworks must be successfully defended.

Homeworks can be done alone or in pairs. Pairs will be formed randomly by the lecturers, separately for each homework. As said, you can always opt to do it alone.

Homework has to be presented during lab time to the lecturer on site: email submissions are not accepted. Both pair members must be present during presentation: in case one of them is not present, the homework of the missing person is not considered to be defended. It is also not guaranteed that both pair members get the same grade.

The homeworks have to be submitted to the university git and then defended: git details will be presented later by Juhan.

Homework deadline policy:

• Defended code must be submitted for defence latest one date before the defence deadline (example: defence deadline 22. Sept, submission 21. Sept).
• In case the homework is defended in time, you have one extra week to add missing details/improvements without losing points.
• In case the homework is not defended in time, you have two extra weeks to defend it, but in this case you will get only half the points.
• No homeworks are accepted after the two extra weeks after the deadline have passed.
• In order to be accepted to exam you have to successfully defend at least three of the four homeworks.

Grades and additional homework info available at https://ained.ttu.ee

Materials for search algorithms

The search algorithms block was based on the following chapters from the book Artificial Intelligence, a Modern Approach, 3rd Edition, by Stewart Russell and Peter Norvig. (The book is available in TUT library as [1] and [2]):

• Chapter 3: Solving problems by searching
• Chapter 4: Beyond classical search
• Chapter 5: Adversarial search
• Chapter 6: Constraint satisfaction problems

In particular, it will be necessary to be able to choose best methods from the ones mentioned in those chapters for solving particular problems. In addition it is necessary to be able to charachterize the properties of these approaches in terms of relevant criteria (branching factor, time complexity, space complexity, completeness).

Course structure

The course will consist of four interconnected blocks covering crucial areas of the subject:

Search algorithms

Homework is available in Moodle. To log in you will need to use your TUT e-mail account in Office 365. You need to form groups yourself and create a repository named iti8600hw1 at Gitlab.cs.ttu.ee. The visibility needs to be "private" and the project should only be shared with the other group member. Access to staff will be granted automatically. Deadline of submission to Gtilab: September 29.

• Tree search, graph search, formulating problems to be solved by search (recap of what you know)
  • The task of the first lab is to pull code from the AIMA Python project and look at the search.py file. You should be able to run the examples shown in the lecture.

• Search 1, Search 2

• Beyond classical search, Constraint solving problems

• Adversarial search (games, minimax, alpha-beta pruning) (OLD VERSION, but content is relevant)

Knowledge representation

Knowledge representation homework 2017: first phase of building a simple question answering system

Useful in-depth material for reading as free pdf-s:

• Knowledge Representation and Reasoning
• Handbook of Knowledge Representation
• Interesting to browse: recent conference proceedings
• Interesting to browse: course materials, course materials, course materials
• course on probabilistic graphical models
• Google natural language processing publications

Three subthemes in four lectures:

Intro, SQL, logic, RDF

Read these:

• First the Lecture presentation
• Second, the first half of the RDF primer
• It is also useful to understand what URI is

Then read:

• Second lecture presentation: RDFS and more
• Facebook social graph
• Facebook Graph Search
• Google knowledge graph
• And explore schema org and schemas

Natural language

• First the Lecture presentation

We have a separate page with useful links and notes on NLP

Also, try out and have a brief look at:

• Try out a very good NER tagger AIDA online. See also the dissertation explaining how AIDA is built.
• Try out part-of-speech tagger
• Have a quick look at Google syntaxnet
• Have a look at the excellent NLTK toolkit tutorial
• Have a look at a tutorial for semantic parsing
• Try out sentiment analysis online
• Have a brief look at a detailed sentiment analysis tutorial

There is a large detailed page with useful links on various NLP tasks.

Representing uncertain knowledge

Lecture material:

• Main part of the uncertainty lecture: beginning and end or as pdf
• Probabilistic and fuzzy reasoning used during the middle part of the lecture.

Additional material:

• default logic Wikipedia on default logic: must read to understand the subject better
• Try out a small nonmonotonic reasoning example
• Formalizing belief and knowledge highly recommended, but not covered in the lecture.
• Bayesian inference recommended if you want to understand Bayesian probabilistic inference
• nonmonotonic logic: long intro to main concepts

You may want to try out the dlv system for answer set programming: usable for implementing default logic.

Just found a cool project with java libraries for different kinds of KR and reasoners.

Reasoning and deduction

Automated reasoning homework 2017: second phase of building a simple question answering system

Deadline 1. december.

Useful books for reading:

• T.Tamme, T.Tammet, R.Prank. Loogika: mõtlemisest tõestamiseni. TÜ Kirjastus, 2002
• coursebook by Geoff or older version as pdf

Test and compare simple propositional solver algorithms:

• logictools.org

Subthemes:

Machine reasoning with first order logic

Lecture material as ppt or as pdf

Additional material:

• wiki intro to resolution
• Fields of automated reasoning and automated theorem proving in wikipedia.
• coursebook by Geoff
• Otter by McCune: use it for experimenting.
• tiny examples of problems for otter
• CASC competition and the TPTP problem library and TPTP problem domains

Propositional solvers

Main material consists of several parts:

• Read the intro - what is first order (FOL) , propositional (SAT) and satisfiability modulo theories (SMT) - and milestones from Nikolaj Bjorner's lecture
• Read the explanation of the DPLL method from the dpll lecture by Agostini and Giunchiglia.
• Read the overview of basic propositional logc solving methods
• Use http://logictools.org/ to experiment with random problems of various sizes and solver algorithms

Additionally you may want to look at:

• DPLL in wikipedia
• regular sat prover competition
• http://minisat.se/

Real and potential applications of reasoners

Lecture material as ppt or as pdf

Additionally you may want to look at (links from the presentation above):

• First order logic: classical stuff
  • Otter solving an open problem in math
  • using otter for algebra problems
  • TPTP problem set for first order logic formalizations
  • set theory and its axiomatization in logic and set theory problems in TPTP
  • CASC prover competition

• Logic and NLP: several approaches
  • Natural logic for NLP at Stanford
  • logical reasoning and NLP
  • combining theorem proving with NLP
  • Inference in NLTK

• Annotated examples of text and sentence derivable from text:
  • Classical FRACAS example set
  • Newer RTE example sets
  • Stanford Question Answering Dataset

SMT solvers

Juhan will give a lecture about SMT solvers and applications: the main family of tools for automated verification.

• Intro to SMT from wikipedia
• SMT tutorial slides (8 first slides were shown in the lecture) alternative slides
• Z3 tutorial in Python, links to binaries etc as compiled by Juhan Ernits.
• The official binary releases of Z3 now include Java support. The example is available here.
• The sample code built during the lecture is available in Moodle.

Learning

Lecture_1_ML_MKBSD_2017.pdf

Lecture_2_ML_MKBSD_2017.pdf

ML_HomeAssignment_2017.pdf

Lecture_3_ML_MKBSD_2017.pdf

Lecture_4_ML_MKBSD_2017.pdf