A Simplified Tableau Calculus for Standpoint LTL

Verfügbar als Thema einer Masterarbeit

Betreuer Tim Lyon
Computational Logic
Beginn
Download

Die lineare temporale Logik (LTL) ist eine modale Logik, die zur Untersuchung temporaler Eigenschaften in der Informatik verwendet wird, während die Standpunktlogik (SL) eine kürzlich eingeführte Multiagentenlogik ist, die unterschiedliche semantische Verpflichtungen erfasst und Schlussfolgerungen mit niedriger Komplexität ermöglicht. Standpunkt-lineare temporale Logik (SLTL) kombiniert das temporale Schließen von LTL mit den multiperspektivischen Möglichkeiten von SL und erlaubt so die Modellierung sowohl der Systementwicklung als auch wechselnder Standpunkte über die Zeit.

Ein zuvor eingeführtes Tableau-Kalkül für SLTL ist strukturell komplex und schwer zu handhaben. Dieses Projekt zielt darauf ab, ein verfeinertes, korrektes, vollständiges und terminierendes Tableau-Kalkül für SLTL zu entwickeln, das sich an Reynolds’ einfacherer Tableau-Methode für LTL orientiert. Dieser neue Ansatz soll das Schlussfolgern in SLTL vereinfachen, ohne dessen Ausdrucksstärke zu beeinträchtigen.

Bitte klicken Sie auf den Download-Link auf der linken Seite, um ein PDF-Dokument zu erhalten, in dem die Ziele und Erwartungen des Projekts beschrieben sind.