en | de

Department of Computer Science
University of Innsbruck
Home Research Teaching Members Events News
Teaching
lectures bachelor projects master projects software
Master Seminar 1
news overview schedule feedback

Master Seminar 1

master program

SE2  WS 2017/2018  703605

Available Topics

AC-KBO

The Knuth-Bendix Order (KBO) is a well-known, fast, and powerful method for proving termination of term rewrite systems. Making KBO applicable to term rewrite systems with associative and commutative symbols (AC-KBO) is a very useful extension that has been repeatedly considered in the literature. The task of this seminar topic is to implement and compare existing variants of AC-KBO. This seminar project can be extended into a master project.

Alpha Avoidance

The λ-calculus is the basis for functional programming languages such as Haskell. Its computation rule (β-reduction) may necessitate renaming of variables (α-conversion):
(λx.xx)(λyz.yz) →β (λyz.yz)(λyz.yz) →β (λz.(λyz.yz)z) ↛β λzz.zz
The task of this seminar topic is to study restrictions of λ-calculus in which the need for α can be avoided. For instance, the first of the β-steps in the example is non-linear [1], the second contracts a downwardly-created redex [2], and the third contracts a redex below an abstraction [3]. Forbidding any of these three, or imposing an appropriate type system [4], suffice to avoid α. What are the mechanisms in play allowing α to be avoided?
  1. BCK-Combinators and Linear λ-Terms have Types
    J.R. Hindley
    Theoretical Computer Science 64, pp. 97 – 105, 1989
  2. Confluence and Superdevelopments
    F. van Raamsdonk
    Proc. 5th International Conference on Rewriting Techniques and Applications, LNCS 690, pp. 168 – 182, 1993
  3. Combinatory Weak Reduction in Lambda Calculus
    N. Çağman, J.R. Hindley
    Theoretical Computer Science 198, pp. 239 – 247, 1998
  4. The Safe Lambda Calculus
    W. Blum, C.-H. Luke Ong
    Logical Methods in Computer Science 5(1), paper 3, 2009
This seminar project can be extended into a master project.

Automating Logarithmic Amortised Complexity Analysis

Based on earlier work on automating amortised complexity analysis, we study the automation of logarithmic amortised complexity, in particular the automation of the (optimal) analysis of self-adjusting data structures like splay trees. This seminar project can be extended into a master project.

Completion for Logically Constrained Rewrite Systems

Knuth-Bendix completion is a fundamental approach in equational theorem proving. If successful, it produces a complete presentation of the theory. Such a presentation allows to decide the word problem, i.e., one can determine for any given equation whether it follows from the input axioms. Complete rewrite systems are thus used by systems like Mathematica to simplify expressions. Recently, the advent of powerful SMT solvers led to the proposal of logically constrained rewriting. This setting is effective and convenient for program analysis as well as to analyse expression rewriting as e.g. done in compilers.
The aim of this project is to formulate a Knuth-Bendix completion procedure for logically constrained rewrite systems. To take advantage of the SMT-related setting, it should be based on the idea of maximal completion, a simple but powerful satisfiability-based completion procedure. This seminar project can be extended into a master project.

Conditional Nonreachability

The question of (general) nonreachability is, given a term rewrite system (TRS) and two terms, is it possible to rewrite an arbitrary substitution instance of the first term into an arbitrary substitution instance of the second term? This kind of nonreachability has applications in termination analysis of TRSs as well as for automatically showing confluence of conditional TRSs. However, for the latter the existing techniques only yield a crude approximation. The task of this seminar topic is to investigate nonreachability analysis for the conditional case, i.e., where the set of axioms may be conditional equations. This seminar project can be extended into a master project.

Deep Learning for Logic

Deep learning is a recent branch of machine learning that has allowed many significant advances in domains such as machine translation, image captioning, speech recognition, or the game of Go. The task of this master seminar topic is to study deep learning and investigate its applicability to recognizing logical formulae. This seminar project can be extended into a master project.

Formalization of Social Choice Theory

Kenneth Arrow showed that every voting scheme with desired properties must necessarily adhere to some undesired restrictions. Amartya Sen introduced a way to prove such results in Social Choice Theory circumventing impossibility results using Social Decision Functions. We will discuss the formalizations of the two results.

Multivariate Amortised Resource Analysis for Term Rewrite Systems

Based on earlier work on automating amortised complexity analysis, we study multivariate amortised resource analysis in the context of term rewrite systems and provide an implementations thereof. This seminar project can be extended into a master project.

Patterns from First- to Higher-Order

Higher-order patterns were introduced by Miller as a subset of the higher-order terms that `behave the same' as in the first-order case. The aim of this seminar is to present the exact meaning of `behaving the same' of the class of patterns of its recent extension with `Functions-as-Constructors'. This concerns issues such as unification and its complexity, but also whether or not the (linear) pattern occurrences in a term constitute a finite distributive lattice, and whether patterns have discriminating power. This seminar project can be extended into a master project.

Proof Terms for Rewriting

Proof terms in term rewriting allow to represent rewrite steps and rewrite sequences as first-order terms. They come equipped with important operations like join and residual. Performing these operations manually is cumbersome and error-prone. The task of this master seminar topic is to study the literature on proof terms and to develop a proof term manipulator for multisteps in left-linear rewrite systems.

Quantified Boolean Formulas

Quantified boolean formulas (QBF) are an extension of propositional logic with explicit quantification over propositional variables. The QBF decision problem is PSPACE-complete. Consequently, many problems from application domains such as model checking that are PSPACE-complete can be encoded in QBF. In the past years significant progress has been made in QBF solving. The aim of this master seminar is to present some of the techniques that have been developed for QBF solving such as QDPLL. This seminar project can be extended into a master project.

Rewriting Techniques for LLVM Expression Optimizations

Compilers draw great advantage from performing so-called peephole optimizations to simplify expressions, as e.g. done in the Instcombine pass of LLVM. Previous work has shown that the current set of LLVM optimizations may loop, thus causing nontermination of the compiler. Besides termination, also unique normal forms of the optimization set is a desirable property to ensure determinism. In order to analyse these properties, rewriting techniques are a natural choice.
In this project we first transform the set of LLVM peephole optimizations into logically constrained term rewrite systems which reflect the intended semantics. Second, termination techniques from the area of constrained rewriting should be applied on the obtained rewrite systems to find terminating subsystems. Some suitable additional techniques should be implemented in the tool Ctrl. This seminar project can be extended into a master project.

Root Isolation and Root Counting of Complex Roots

Complex root isolation is the task to compute a number of discs in complex space for a given polynomial, such that each disc contains precisely one root. This task has applications in algebraic geometry, for instance in the implementation of complex algebraic numbers. One approach to complex root isolation is bisection in combination with a root counting method, where root counting demands to compute the number of roots for a given disc and polynomial.
The aim of this master seminar is to present existing root counting and root isolation algorithms for complex numbers such as Kronecker's method. This seminar project can be extended into a master project.

Machine Learning Problems in Automated Reasoning

Cezary Kaliszyk

In this talk I will discuss the ATP tasks which correspond to machine learning problems. I will define internal guidance, and discuss the existing approaches to integrating such guidance in various automated reasoning calculi. We will look at prediction of the actual inference rules to apply at a given proof step, as well as at more powerful state evaluation functions and conjecturing of possible useful intermediate ATP steps.

Normalising Strategies for Orthogonal Systems and Beyond

Vincent van Oostrom

A strategy for a term rewrite system is normalising if for any term having a normal form, that normal form is found by repeated execution of the strategy. In this talk we will first address the question how to find a normalising strategy for term rewrite systems, and next how to prove that such a strategy in fact is normalising. We revisit and refine strategies introduced by Huet and Lévy contracting, respectively,
  1. external (an outer redex having an external residual),
  2. linear (a redex having one linear residual), or
  3. needed (redexes having at least one needed residual)
redexes. We extend our earlier analysis for left-normal term rewrite system, e.g. CL and lambda-beta-calculus, to orthogonal term rewrite systems first, and to some non-orthogonal systems, e.g. lambda-beta-eta-calculus and lambda-calculi with explicit substitutions, next.

The Perron–Frobenius Theorem for Certification of Complexity Proofs

René Thiemann

Matrix interpretations are widely used in automated complexity analysis. Certifying such analyses boils down to determining the growth rate of An for a fixed non-negative rational matrix A. A direct solution for this task involves the computation of all eigenvalues of A, which often leads to expensive algebraic number computations. Therefore, we will illustrate in this talk how the required computations can be simplified with the help of variants of the Perron–Frobenius theorem, and further provide some details on the formalization.

Artificial Intelligence for Perfect Information Games

Thibault Gauthier

We present the progress of artificial intelligence in two-player zero-sum perfect information games such as draughts, chess and go. We observe the gradual optimization of tree search algorithms and describe them in terms of changes to their policy (choosing a move) and evaluation (estimating a position) functions. This journey culminates in the introduction of deep learning and reinforcement learning techniques that were crucial to win against the best humans at the game of go.

Legendrian Racks: where automated theorem proving meets contact topology

T. V. H. Prathamesh

Finding `invariants' of geometric objects under deformations is one of the key areas of research in topology/geometry. These invariants range from numbers and polynomials associated to the object, to algebraic structures such as groups. In this talk, I will discuss an invariant of a class of knots called Legendrian knots, called Legendrian racks. Legendrian knots are an object of interest to topologists studying contact topology. Legendrian racks are an example of algebraic structures called racks, which are self-distributive structures and finitely axiomatizable in first-order logic. Thus it could possibly be of interest from a term rewriting perspective.
The discovery of these invariants was aided by the use of the first-order theorem prover Prover9. It was inspired by an earlier work by Fish and Lisitsa, on using automated theorem provers for unknot recognition.
In this talk, I will discuss Legendrian racks, and how Prover9 aided the discovery of these invariants. That talk will be largely self-contained, and no background in topology/geometry or knot theory will be assumed.

Complexity Analysis for Extended First Epsilon Theorem

Kenji Miyamoto

Hilbert's pure epsilon calculus is elementary calculus extended with the epsilon operator ε, and further enriched by the equality predicate. The epsilon operator allows to express for a given formula A(x) a term εxA(x) whose property is characterized by the critical axiom A(t)→A(εxA(x)) where t is an arbitrary term. Extended epsilon theorem by Hilbert and Bernays claims that if a formula A(e) is true in pure epsilon calculus for a term e which may involve ε, there are some number n and ε-free terms s1, ..., sn such that A(s1) ∨ ... ∨ A(sn) is true in elementary calculus. This theorem is understood as an admissibility result similar to the cut elimination theorem, and moreover the numerical bound of the number n expresses the complexity of the critical axiom. I am going to talk about the current results in complexity analysis for extended first epsilon theorem involving the equality predicate. This is joint work with Georg Moser.

Proof-of-Stake Blockchain Security

Michael Färber

Running Proof-of-Work blockchain protocols is relatively energy-consuming. Alternatives such as Proof-of-Stake protocols solve this problem, but so far, the security of such systems has not been rigorously analysed. I summarise a paper which introduces a new Proof-of-Stake blockchain protocol as well as proves several security properties of it.

Relative Definability of Higher-order Functions in Simply Typed Lambda Calculus

Evan Marzion

Clone theory may be viewed as a way of studying definability between first-order functions within the presence of certain natural operations, namely projection and composition. The founding result from clone theory is Post's complete classification of the lattice of clones over the two element boolean domain, from which his functional completeness theorem falls out. In this talk, we will show how to extend this work in order to accommodate higher-order functions. We will briefly recount Post's work before introducing a higher-order analog to clones, which we call a combinatory clone. A combinatory clone can be thought of as a set of functions which is closed under definability in the simply-typed lambda calculus. We will show how a number of results from Post's work transfer over into this higher-order setting, while also highlighting when things differ.

A Formally Verified Solver for Homogeneous Linear Diophantine Equations

Christian Sternagel

I will present an Isabelle/HOL formalization of homogeneous linear diophantine equations, focusing on an algorithm for computing minimal complete sets of solutions. I will start from a simple but inefficient variant of Huet's lexicographic algorithm incorporating improved bounds due to Clausen and Fortenbacher. Then, I will employ program transformation techniques to obtain a reasonably efficient implementation.

Completeness of Inst-saturated Sets of First Order Clauses with Equality

Alexander Maringele

Instantiation-based theorem proving eventually finds a finite set of unsatisfiable ground instances for any unsatisfiable set of first order clauses (at least in theory). Satisfiability of ground instances can be effectively decided by a SAT-solver. But in general, satisfiability of a finite set of ground instances does not confirm the satisfiability of a set of non-ground clauses. Unit paramodulation is part of a sound instantiation-based calculus for first order logic with equality. The proving procedure may saturate without generating an unsatisfiable set of ground instances. We present a completeness proof from the literature. An Inst-saturated set of non-ground clauses with satisfiable grounded instances is satisfiable.

ENIGMA: Efficient Learning-Based Inference Guiding Machine

Jan Jakubův

ENIGMA is a learning-based method for guiding given clause selection in saturation-based theorem provers. Clauses from many previous proof searches are classified as positive and negative based on their participation in the proofs. An efficient classification model is trained on this data, classifying a clause as useful or un-useful for the proof search. This learned classification is used to guide next proof searches prioritizing useful clauses among other generated clauses. The approach is evaluated on the E prover and the CASC 2016 AIM benchmark, showing a large increase of E's performance.

Formalizing Completeness of Ordered Completion

Sarah Winkler

Ordered completion, also known as unfailing completion, is a landmark method in equational theorem proving. An ordered completion procedure outputs a ground complete system which can be used to decide the validity problem on ground terms. Already when proposing ordered completion in 1989, Bachmair, Dershowitz, and Plaisted showed that under certain circumstances ordered completion results in a complete system, which can thus also be used to decide the validity problem on open terms. Devie later on proved a more general result for linear systems. The talk is about the formalization of these completeness results in IsaFoR.

Proof Strategy Language and Proof Method Recommendation

Yutaka Nagashima

Despite the recent progress in automatic theorem provers, proof engineers are still suffering from the lack of powerful proof automation. In this talk, I present a proof strategy language (PSL) and a proof method recommendation tool (PaMpeR) for Isabelle/HOL. Given a strategy and a proof obligation, PSL generates and combines various tactics to search for a proof script. On the contrary, PaMpeR recommends proof methods to discharge the proof goal without conducting a proof search by using a decision tree algorithm.

FORT 2.0

Franziska Rapp

In this talk I will present the newest version of our tool FORT. It is a decision and synthesis tool for the first-order theory of rewriting with the restriction to left-linear right-ground TRSs. In particular it is now possible to express commutation and other properties on multiple TRSs. The inspiring tool for this extension was Carpa, which is quite strong on synthesizing ARSs, but cannot handle left-linear right-ground TRSs.

Layer Systems for Confluence — Formalized

Bertram Felgenhauer

Layer systems are a common framework for proving several related results on confluence of term rewrite systems, including modularity of confluence, persistence of confluence, and preservation of confluence by currying. I will talk about a formalization of layer systems in Isabelle, as part of IsaFoR.

Towards a Hardware-Parallel Implementation of Interaction Nets

David Obwaller

Interaction nets are a computational model based on graph rewriting and allow for parallel and asynchronous reduction. Interaction automata serve as environment for concrete implementations of parallel (potentially abstract) hardware, that can be used to run interaction net computations. I will talk about interaction nets, interaction automata, and related frameworks and techniques for executing parallel programs