A Simplified Tableau Calculus for Standpoint LTL

Available as topic for a Master's thesis

Supervisor Tim Lyon
Computational Logic
Start
Download

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.

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.

Please click the download link to the left for a PDF document that details the goals and expectations of the project.