Thema3516: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
(Die Seite wurde neu angelegt: „{{Abschlussarbeit |Titel DE=A Simplified Tableau Calculus for Standpoint LTL |Titel EN=A Simplified Tableau Calculus for Standpoint LTL |Abschlussarbeitstyp=Master |Betreuer=Tim Lyon |Forschungsgruppe=Computational Logic |Abschlussarbeitsstatus=Offen |Beschreibung DE=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 einge…“) |
Keine Bearbeitungszusammenfassung |
||
| Zeile 8: | Zeile 8: | ||
|Beschreibung DE=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. | |Beschreibung DE=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. | ||
<br> | <br> | ||
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. | 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. | ||
<br> | <br> | ||
| Zeile 15: | Zeile 14: | ||
|Beschreibung EN=Linear temporal logic (LTL) is a modal logic used for reasoning about temporal properties in computing, while standpoint logic (SL) is a recently introduced multi-agent logic that captures differing semantic commitments and offers low-complexity reasoning. Standpoint linear temporal logic (SLTL) combines the temporal reasoning of LTL with the multi-perspective capabilities of SL, allowing for the modeling of both system evolution and changing standpoints over time. | |Beschreibung EN=Linear temporal logic (LTL) is a modal logic used for reasoning about temporal properties in computing, while standpoint logic (SL) is a recently introduced multi-agent logic that captures differing semantic commitments and offers low-complexity reasoning. Standpoint linear temporal logic (SLTL) combines the temporal reasoning of LTL with the multi-perspective capabilities of SL, allowing for the modeling of both system evolution and changing standpoints over time. | ||
<br> | <br> | ||
A tableau calculus was previously introduced for SLTL but is structurally complex and difficult to use. This project aims to develop a refined, sound, complete, and terminating tableau calculus for SLTL, modeled after Reynolds’s simpler tableau system for LTL. This new approach seeks to streamline reasoning in SLTL while maintaining its expressive power. | A tableau calculus was previously introduced for SLTL but is structurally complex and difficult to use. This project aims to develop a refined, sound, complete, and terminating tableau calculus for SLTL, modeled after Reynolds’s simpler tableau system for LTL. This new approach seeks to streamline reasoning in SLTL while maintaining its expressive power. | ||
<br> | <br> | ||
Version vom 28. März 2025, 14:15 Uhr
A Simplified Tableau Calculus for Standpoint LTL
Verfügbar als Thema einer Masterarbeit
- Betreuer Tim Lyon
- Computational Logic
- Beginn
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.
