Thursday 22nd June 2017, 3:00pm
CIIRC building A, 6th floor, room A623 at Jugoslávských partyzánů 1580/3, Prague 6

Jet Engine Software
In this talk, I explain how computers control modern jet engines, and how they manage to keep them safe and reliable. I briefly explain how a jet engine works, before covering some basics about engine control hardware and software architecture. I then go on to talk about the software development processes that are typically employed.

Friday 16th June 2017, 2:30pm
CIIRC building A, 6th floor, room A623 at Jugoslávských partyzánů 1580/3, Prague 6


Friday 26th May 2017, 2:30pm
CIIRC building A, 6th floor, room A623 at Jugoslávských partyzánů 1580/3, Prague 6

"What I have been doing during my spring vacation in Prague"

Tuesday 27th December 2016, 2:00pm
BLOX building 6th floor at Evropská 2785/11, Prague 6

The mystery of QBF tautologies
A tautological clause is a clause which contains both a literal and its complement.
While in the classical setting of propositional and firstorder logic tautologies are harmless
(in the sense that they are always vacuously satisfied and thus can be safely discarded),
in the study of resolutionbased calculi for quantified boolean formulas (QBF)
we encounter tautologies which can be harmful (their generation is explicitly prohibited,
because they would make the calculus unsound), but also useful
(the longdistance resolution calculus gains exponential power over
Qresolution by allowing generation of certain tautologies). I will try to shed light
on this discrepancy through the lens of the translation of QBF to firstorder logic proposed
by Seidl et al. (2012). This should also motivate a discussion about the currently missing
local semantics of a clause within the context of QBF resolutionbased calculi.

Monday 14th November 2016, 2:00pm
BLOX building 6th floor at Evropská 2785/11, Prague 6


Monday 31st October 2016, 2:00pm
BLOX building 6th floor at Evropská 2785/11, Prague 6


Tuesday 25th October 2016, 12:45am
BLOX building 8th floor at Evropská 2785/11, Prague 6

Lifted Relational Neural Networks
We propose a method combining relationallogic representations with neural network learning. A general lifted architecture, possibly reflecting some background domain knowledge, is described through relational rules which may be handcrafted or learned. The relational ruleset serves as a template for unfolding possibly deep neural networks whose structures also reflect the structures of given training or testing relational examples. Different networks corresponding to different examples share their weights, which coevolve during training by stochastic gradient descent algorithm. The framework allows for hierarchical relational modeling constructs and learning of latent relational concepts through shared hidden layers weights corresponding to the rules. Discovery of notable relational concepts and experiments on 78 relational learning benchmarks demonstrate favorable performance of the method.

Thursday 14th July 2016, 2:00pm
BLOX building 6th floor at Evropská 2785/11, Prague 6


Monday 30th May 2016, 2:00pm
BLOX building 6th floor at Evropská 2785/11, Prague 6

Knot recognition by SAT and ATP

Friday 6th May 2016, 1:30pm
BLOX building 6th floor at Evropská 2785/11, Prague 6

Initial Experiments with Neural Networks using TensorFlow Framework

Friday 1st April 2016, 2:30pm
BLOX building 6th floor at Evropská 2785/11, Prague 6

Prover9 and Solving Open Problems Using Hints

Wednesday 9th March 2016, 11:00am
BLOX building 6th floor at Evropská 2785/11, Prague 6

Concept Matching Between Formal Libraries

Friday 4th March 2016, 11:00am
BLOX building 6th floor at Evropská 2785/11, Prague 6

Finding Finite Models in MultiSorted First Order Logic

Friday 19th February 2016, 2:30pm
BLOX building 6th floor at Evropská 2785/11, Prague 6


Monday 7th April 2014, 4:15pm
Room 112

Multiagent Planning by Iterative Negotiation over Distributed Planning Graphs  Part 2
Deterministic multiagent planning described by MASTRIPS
formalism requires mixture of coordination and synthesis of
local agents' plans. All agents' plans, as sequences of actions, can be
implicitly described by an appropriate generative structure. Having
all local plans of all participating agents described by such a structure
and having a merged process of such structures, we can induce a
global multiagent plan by successive elimination of unfeasible combinations
of local agents' plans.
In this paper, we propose use of Nondeterministic Finite StateMachines
(NFSs) as the generative structure for the plans and use of
wellknown process of intersection of NFSs to prune the plan spaces
towards globally feasible multiagent plan. Since the numbers of the
plans can be large we use iterative process of building of the NFSs
using a stateoftheart classical planner interleaved with the NFS intersecting
process. To show efficiency of the approach, we have evaluated
the algorithm on extensive number of planning problems from
Internation Planning Competition extended for multiagent planning.

Monday 24th March 2014, 4:15pm
Room 112

Multiagent Planning by Iterative Negotiation over Distributed Planning Graphs  Part 1
Deterministic multiagent planning described by MASTRIPS
formalism requires mixture of coordination and synthesis of
local agents' plans. All agents' plans, as sequences of actions, can be
implicitly described by an appropriate generative structure. Having
all local plans of all participating agents described by such a structure
and having a merged process of such structures, we can induce a
global multiagent plan by successive elimination of unfeasible combinations
of local agents' plans.
In this paper, we propose use of Nondeterministic Finite StateMachines
(NFSs) as the generative structure for the plans and use of
wellknown process of intersection of NFSs to prune the plan spaces
towards globally feasible multiagent plan. Since the numbers of the
plans can be large we use iterative process of building of the NFSs
using a stateoftheart classical planner interleaved with the NFS intersecting
process. To show efficiency of the approach, we have evaluated
the algorithm on extensive number of planning problems from
Internation Planning Competition extended for multiagent planning.

Monday 10th March 2014, 4:15pm
Room 112

Lemma mining over HOL Light
Large formal mathematical libraries consist of millions of atomic inference steps that give rise to a corresponding number of proved statements (lemmas). Analogously to the informal mathematical practice, only a tiny fraction of such statements is named and reused in later proofs by formal mathematicians. In this work, we suggest and implement criteria defining the estimated usefulness of the HOL Light lemmas for proving further theorems. We use these criteria to mine the large inference graph of all lemmas in the core HOL Light library, adding thousands of the best lemmas to the pool of named statements that can be reused in later proofs. The usefulness of the new lemmas is then evaluated by comparing the performance of automated proving of the core HOL Light theorems with and without such added lemmas.

Monday 18th November 2013, 4:05pm
Room 112

Undecidability of Consequence Relation in Full Nonassociative Lambek Calculus
We prove that the consequence relation in the Full Nonassociative Lambek calculus is undecidable. An encoding of the halting problem for 2tag systems using finitely many nonlogical axioms in the language {⋅,∨} will be presented. Therefore already the consequence relation in this fragment is undecidable. Moreover, the construction works even when the structural rules of exchange and contraction are added.

Monday 21st October 2013, 4:05pm
Room 112

Automated Generating of Hypotheses by Genetic Algorithms

Monday 7th October 2013, 4:15pm
Room 112

Automated Reasoning Service for HOL Light
HOL(y)Hammer is an AI/ATP service for formal (computerunderstandable) mathematics encoded in the HOL Light system, in particular for the users
of the large Flyspeck library. The service uses several automated reasoning systems combined with several premise selection
methods trained on previous Flyspeck proofs, to attack a new conjecture that uses the concepts defined in the Flyspeck library. The public online
incarnation of the service runs on a 48CPU server, currently employing
in parallel for each task 25 AI/ATP combinations and 4 decision procedures that contribute to its overall performance. The system is also
available for local installation by interested users, who can customize it for their own proof development. An Emacs interface allowing parallel
asynchronous queries to the service is also provided. The overall structure of the service is outlined, problems that arise are discussed, and an
initial account of using the system is given.

Monday 29th April 2013, 4:15pm
Room 112

General Bindings and AlphaEquivalence in Nominal Isabelle
Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem prover. It provides a proving infrastructure for reasoning about programming language calculi involving named bound variables (as opposed to deBruijn indices). In this paper we present an extension of Nominal Isabelle for dealing with general bindings, that means termconstructors where multiple variables are bound at once. Such general bindings are ubiquitous in programming language research and only very poorly supported with single binders, such as lambdaabstractions. Our extension includes new definitions of alphaequivalence and establishes automatically the reasoning infrastructure for alphaequated terms. We also prove strong induction principles that have the usual variable convention already built in.

Monday 18th March 2013, 4:15pm
Room 112


Monday 4th March 2013, 4:15pm
Room 112

Duality in STRIPS planning II
We describe a duality mapping between STRIPS planning tasks. By exchanging the initial and goal conditions, taking their respective complements, and swapping for every action its precondition and delete list, one obtains for every STRIPS task its dual version, which has a solution if and only if the original does. This is proved by showing that the described transformation essentially turns progression (forward search) into regression (backward search) and vice versa.
The duality sheds new light on STRIPS planning by allowing a transfer of ideas from one search approach to the other. It can be used to construct new algorithms from old ones, or (equivalently) to obtain new benchmarks from existing ones. Experiments show that the dual versions of IPC benchmarks are in general quite difficult for modern planners. This may be seen as a new challenge. On the other hand, the cases where the dual versions are easier to solve demonstrate that the duality can also be made useful in practice.

Monday 18th February 2013, 4:15pm
Room 112

Duality in STRIPS planning I
We describe a duality mapping between STRIPS planning tasks. By exchanging the initial and goal conditions, taking their respective complements, and swapping for every action its precondition and delete list, one obtains for every STRIPS task its dual version, which has a solution if and only if the original does. This is proved by showing that the described transformation essentially turns progression (forward search) into regression (backward search) and vice versa.
The duality sheds new light on STRIPS planning by allowing a transfer of ideas from one search approach to the other. It can be used to construct new algorithms from old ones, or (equivalently) to obtain new benchmarks from existing ones. Experiments show that the dual versions of IPC benchmarks are in general quite difficult for modern planners. This may be seen as a new challenge. On the other hand, the cases where the dual versions are easier to solve demonstrate that the duality can also be made useful in practice.

Wednesday 2nd January 2013, 1:30pm
Room 112

Executing HOL Project in the Isabelle theorem prover
In Isabelle/HOL, code generation is understood as the transformation of a system of equational theorems into a program in a functional programming language with the same equational semantics. This guarantees partial correctness of generated programs.
This generic framework is instantiated for SML, OCaml and Haskell. The metatheory permits program and datatype refinement, i.e. the replacement of abstract algorithms and representations by efficient and executable programs and data structures . without endangering partial correctness.
On top of this, the scope of executable specifications can be extended by providing tools which produce suitable equational specifications from theories. An example is a predicate compiler which turns inductive specifications into equational ones, thus opening the world of functionallogic programming for code generation.
Additionally, we have provided Haskabelle which transforms a subset of Haskell to Isabelle/HOL theory text.

Monday 21st January 2013, 4:15pm
Room 112


Friday 21st December 2012, 4:00pm
Room 112

On Propositional QBF Expansions and QResolution
Over the years, proof systems for propositional satisfiability (SAT) have been extensively studied. Recently, proof systems for quantified Boolean formulas (QBFs) have also been gaining attention. Qresolution is a calculus enabling producing proofs from DPLLbased QBF solvers. While DPLL has become a dominating technique for SAT, QBF has been tackled by other complementary and competitive approaches. One of these approaches is based on expanding variables until the formula contains only one type of quantifier; upon which a SAT solver is invoked. This approach motivates the theoretical analysis carried out in this paper. We focus on a two phase proof system, which expands the formula in the first phase and applies propositional resolution in the second. Fragments of this proof system are defined and compared to Qresolution.

Monday 3rd December 2012, 4:15pm
Room 112

ATP over Flyspeck
The considerable mathematical knowledge encoded by the Flyspeck project is combined with external automated theorem provers (ATPs) and machinelearning premise selection methods trained on the proofs, producing an AI system capable of answering a wide range of mathematical queries automatically. The performance of this architecture is evaluated in a bootstrapping scenario emulating the development of Flyspeck from axioms to the last theorem, each time using only the previous theorems and proofs. It is shown that 39% of the 14185 theorems could be proved in a pushbutton mode (without any highlevel advice and user interaction) in 30 seconds of real time on a fourteenCPU workstation. The necessary work involves: (i) an implementation of sound translations of the HOL Light logic to ATP formalisms: untyped firstorder, polymorphic typed firstorder, and typed higherorder, (ii) export of the dependency information from HOL Light and ATP proofs for the machine learners, and (iii) choice of suitable representations and methods for learning from previous proofs, and their integration as advisors with HOL Light. This work is described and discussed here, and an initial analysis of the body of proofs that were found fully automatically is provided.

Monday 19th November 2012, 4:15pm
Room 112

Semantic guidance for unbounded symbolic reachability

Monday 5th November 2012, 4:15pm
Room 112

Scheduling with and without Z3
