- Isolde Adler, Goethe-Universität Frankfurt am Main
- Frederik Harwath,
- André Hernich, Goethe-Universität Frankfurt am Main
- Martin Hofmann, LMU München:
Pure Pointer Programs and Logspace
- Ahmet Kara, TU Dortmund:
On the Hybrid Extension of CTL and CTL+
[ Abstract:
]
Abstract
The paper studies the expressivity, relative succinctness and complexity of satisfiability for hybrid extensions of the branching-time logics CTL and CTL+ by variables. Previous complexity results show that only fragments with one variable do have elementary complexity. It is shown that H1CTL+ and H1CTL, the hybrid extensions with one variable of CTL+ and CTL, respectively, are expressively equivalent but H1CTL+ is exponentially more succinct than H1CTL. On the other hand, HCTL+, the hybrid extension of CTL with arbitrarily many variables does not capture CTL*, as it even cannot express the simple CTL* property EGFp. The satisfiability problem for H1CTL+ is complete for triply exponential time, this remains true for quite weak fragments and quite strong extensions of the logic.
- Markus Krötzsch, Karlsruhe Institute of Technology
When Ontologies Meet Rules: Integrating Description Logics and Horn Logic
- Jiamou Liu, Universität Leipzig:
The Isomorphism Problem on Classes of Automatic Structures
[ Abstract
]
Abstract
A structure is automatic if its elements are coded in such a way that
its domain and relations are recognizable by finite automata. The
isomorphism problem on a class K of automatic structures calls for an
algorithm that decides, for any given two automatic structures A,B in K,
whether A is isomorphic to B. In this talk we present our new results
on the isomorphism problem for some typical classes of automatic structures. In particular,
we prove the following:
1. The isomorphism problem for automatic equivalence structures is
undecidable (in fact \Pi^0_1-complete)
2. The isomorphism problem for automatic trees of height h is
\Pi^0_{2h-3}-complete (h>1).
3. The isomorphism problem for automatic linear orders is not arithmetic
(hard for every level of the arithmetic hierarchy).
- Markus Lohrey, Universität Leipzig
- Conrad Rau, Goethe-Universität Frankfurt am Main
- Sebastian Rudolph, Karlsruhe Institute of Technology:
Decidability of Conjunctive Queries in Description Logics with Inverses, Counting and Nominals
- David Sabel, Goethe-Universität Frankfurt am Main:
Proof Methods for Polymorphically Typed Contextual Equivalence
[ Abstract:
]
Abstract
We describe syntactical proof methods for contextual equivalence in
polymorphically typed lambda-calculi.
Our example calculus has cyclic let, data constructors, case-expressions, seq, and recursive types.
The polymorphically typed language is a subset of the untyped language.
We use (call-by-need) normal-order reduction on untyped expressions as operational semantics, and
as a proof technique we use type-labels for all subexpressions and a typed normal order reduction which
preserves the type labeling of expressions.
As we show this technique allows us to prove a context lemma for the type-labeled calculus,
and to reason about correctness of (typed) program transformations in the typed language by using so-called
forking and commuting diagrams. This is joint work with Manfred Schmidt-Schauß and Frederik Harwath.
- Manfred Schmidt-Schauß, Goethe-Universität Frankfurt am Main:
Reconstruction of a Logic for Functional Programs
- Peter H. Schmitt, Universität Karlsruhe
- Nicole Schweikardt, Goethe-Universität Frankfurt am Main:
Addition-invariant first order and regular languages
- Thomas Schwentick, TU Dortmund
- Jan Schwinghammer, Universität des Saarlandes:
Nested Hoare Triples and Frame Rules for Higher-order Store - Helmut Seidl, TU München
- Christoph Walther, TU Darmstadt
