# Tuesday seminar on artificial intelligence

**Time:**Tuesday, 10:40

**Place:**S8, Malá Strana.

A seminar that aims to refer on ongoing research projects of participants and related issues within the scope of artificial intelligence, theoretical computer science and mathematical logic. Presentation should be for 60 minutes and follow-up discussion is expected. If you, your student or your guess would like to give a talk, then let me know to schedule it.

Students can enroll this seminar as the course NTIN091 (Seminar for MSc. and Ph.D.-students).

## Winter semester 2022/23

- 4.10. Cancelled
- 18.10. Marta Vomlelová: Active learning

Gathering labeled data is often difficult. Active learning assumes the 'easy to get' unlabeled data, for example web pages. Then, a selection strategy iteratively selects an unlabeled example to classify by an expert (oracle). Several strategies are studied. They are based on the probability distribution estimate, the risk difference estimate, the expected error reduction and others. - 25.10. Jiří Švancara: Multi-agent pathfinding

The classical multi-agent pathfinding is the task of navigating a set of agents in a shared environment from their start locations to their desired goal locations. In this talk, we present the history of the problem, the most popular solving approaches, and some of our results. Mainly, we will focus on solving the classical problem optimally using reduction to SAT, then we present some practical extensions of MAPF so that it is more directly applicable to real-world problems such as autonomous intersections, warehousing, robot navigation, and much more. - 1.11. Cancelled
- 15.11. Jakub Bulín: Few subpowers and short definitions

A relation S is pp-definable from a set of relations {R_1, R_2, ...} if it is definable by an existentially quantified conjunction of predicates, or equivalently, if it is invariant under all functions that preserve all the relations R_i. Motivated by the CSP, Berman, Idziak, Markovic, McKenzie, Valeriote, and Willard [Trans. AMS & SICOMP 2010] discovered the importance of the following property: {R_1, R_2, ...} has few subpowers, if the number of n-ary pp-definable relations is bounded by 2^p(n),for some polynomial p. Few subpowers can be seen as a generalization of "linear algebra", i.e., properties of affine subspaces over a finite field, and indeed, CSP for few subpowers can be solved by a "Gaussian eliminiation"-like algorithm. Let us consider the following related property: let us say that {R_1, R_2, ...} has short definitions if every n-ary pp-definable S can be defined by formula of length bounded by p(n), for some polynomial p. We will discuss the open question whether few subpowers imply short definitions, partial results towards a positive answer, and several related open problems. - 22.11. Cancelled
- 29.11. Ondřej Čepek: Knowledge representation languages and knowledge compilation

In this talk we survey several types of knowledge representation languages (Boolean formulas, binary decision diagrams, list-based representations, Boolean circuits, and negational normal forms) and compilation among these languages. The talk is based mainly on the Knowledge Compilation Map framework [Darwiche and Marquis, 2002] and several recent extensions of this framework. - 13.12. Cancelled
- 20.12. Cancelled
- 3.1. Cancelled

## Summer semester 2022/23

- Adam Dingle: Automatically checking proofs in controlled natural language using higher-order logic

In most interactive theorem-proving systems, the user must build a proof script that looks something like a computer program. By contrast, I have been developing a new theorem prover in which the input format looks like mathematical English, written with a limited vocabulary and grammar. The prover translates the input into formulas of higher-order logic, which it then either attempts to prove directly or can export to external higher-order provers. Starting with the Peano Postulates as axioms, the system is already capable of verifying various arithmetic identities. In this talk I will demonstrate this system and will discuss its logical foundation, its controlled natural language input format, and how the system translates and proves theorems.