Hierarchies in Guarded Team Logics

Logics with team semantics are expressive logics whose main feature is that formulae are evaluated by sets of assignments called "teams". This makes it easy to model interdependencies between assignments as atomic properties. Guarded logics are a class of logics where assignments have to be "guarded". Essentially, this means that we cannot assign arbitrary elements to free variables. Instead, they have to appear together in a relation. This yields logics that are robustly decidable.

This work introduces a new type of team logic called hybrid team logic whose variants have the same expressive power as some important established team logics. Instead of team atoms, it features binders that "store" a team in a relational variable.

Further, we combine guarded and team semantics and analyse the expressive power of the resulting logics. This yields an expressive hierarchy that is significantly more complex than the non-guarded case. Notably, guarded hybrid logics are, in general, more expressive than their atom-based counterpart while retaining the desirable model-theoretic properties of guarded logics.

Logiken mit Team-Semantik sind ausdrucksstarke Logiken deren Hauptmerkmal es ist, dass Formeln von Zuweisungsmengen ausgewertet werden, die "Teams" genannt werden. Das macht es einfach, Zusammenhänge zwischen Zuweisungen als atomare Eigenschaften zu modellieren. Die Klasse der "bewachten" Logiken (engl.\ guarded logics) zeichnet sich dadurch aus, dass Zuweisungen "bewacht" sein müssen. Im Wesentlichen bedeutet das, dass Elemente nicht willkürlich zugewiesen werden können, sondern nur, wenn sie gemeinsam in einer Relation vorkommen. Dadurch entstehen Logiken, die robust entscheidbar sind.

Diese Arbeit führt einen neuen Typ Team-Logiken namens hybride Team-Logiken ein, dessen Varianten dieselbe Ausdrucksstärke wie einige wichtige etablierte Team-Logiken haben. Statt Team-Atomen werden hier "binder" verwendet, die ein Team in einer relationalen Variable "speichern".

Weiterhin verbinden wir bewachte und Team-Semantik und analysieren die Ausdrucksstärke der resultierenden Logiken. Daraus ergibt sich eine Hierarchie der Ausdrucksstärke, die signifikant komplexer ist als im nicht-bewachten Fall. Insbesondere sind bewachte hybride Team-Logiken (im Allgemeinen) stärker als ihr Atom-basiertes Gegenstück und erhalten gleichzeitig die wünschenswerten modelltheoretischen Eigenschaften von bewachten Logiken.