TeReSe 2019

Reasoning about one-sided and two-sided infinite sequences.
Hans Zantema
(abstract)

We recapitulate first order inductive theorem proving in a general setting without requirements on the shape of the equations involved. We show how this applies to settings in which the terms on which induction is applied do not have a unique representation as constructor terms. In this way we can do induction over the integers rather than over the natural numbers. We show how this induction mechanism can be applied to prove equality of infinite sequences, and how this is closely related to circular coinduction. As one-sided sequences can be defined as mappings from natural numbers to some basic type, we can also consider two-sided infinite sequences being mappings from integers to the base type, and apply the induction principle over the integers to prove equality of these. In particular we consider a two-sided variant of morphic sequences.

Proving Non-Termination via Loop Acceleration
Florian Frohn
Joint work with Jürgen Giesl
(abstract)

We present a new approach to prove non-termination of integer programs. It is based on a novel under-approximating loop acceleration technique, a new sufficient criterion to detect non-termination, and an SMT encoding to search for invariants. To evaluate our technique, we implemented it in our tool LoAT. A comparison with other leading termination analyzers for integer programs shows that it is competitive and can prove non-termination of some programs where existing tools fail.

Higher-order Polymorphic Polynomials
Cynthia Kop
Joint work with Łukasz Czajka (also to be presented at FSCD 2019)
(abstract)

We generalise the termination method of higher-order polynomial interpretations to a setting with impredicative polymorphism. Instead of using weakly monotonic functionals, we interpret terms in a suitable extension of System Fω. This enables a direct interpretation of rewrite rules which make essential use of impredicative polymorphism. In addition, our generalisation eases the applicability of the method in the non-polymorphic setting by allowing for the encoding of inductive data types. As an illustration of the potential of our method, we prove termination of a substantial fragment of full intuitionistic second-order propositional logic with permutative conversions.

Constant Runtime Complexity of Term Rewriting is Semi-Decidable
Jürgen Giesl
Joint work with Florian Frohn
(abstract)

We show that it is semi-decidable whether the runtime complexity of a term rewrite system is constant. Our semi-decision procedure exploits that constant runtime complexity is equivalent to termination of a restricted form of narrowing, which can be examined by considering finitely many start terms. We implemented our semi-decision procedure in the tool AProVE to show its efficiency and its success for systems where state-of-the-art complexity analysis tools fail.

The Embedding Path Order for Lambda-Free Higher-Order Terms
Alexander Bentkamp
(abstract)

I will present a variant of RPO for higher-order terms without lambda-abstractions. Being a ground-total simplification order, it appears promising for higher-order superposition. I developed an algorithm to compute the order reasonably fast and implemented it in the Zipperposition theorem prover.