Reasoning in temporal logic is important in many areas of AI. This tutorial provides a detailed overview of tableau methods, an important kind of reasoning techniques, with a focus on both theoretical properties and practical applications.
Temporal logic is one of the most used formalisms to express properties of computations, plans, processes, in AI, formal verification and other fields. Reasoning in temporal logic is one of the most studied task in the literature. Tableau methods are among the first reasoning techniques studied for this purpose, and provide both interesting theoretical insights and practical algorithmic techniques. Despite being a field that has been studied for decades, development of tableau methods for temporal logics continues to this date. In particular, while classic tableau methods for linear-time temporal logics are graph-shaped, recently much work have been focused on tree-shaped tableaux, which proved to have many practical advantages. This tutorial aims at providing a detailed overview of classical results and recent advanced developments in the area of tableau methods for linear-time temporal logics. Focus will be given on both theoretical foundations and practical aspects, from classic graph-shaped tableaux to recent tree-shaped ones, and their recent SAT encodings. All the topics will be introduced together with their needed background, hence no particular prerequisite is needed to attend the tutorial. The treated topics can be of interest to researchers and practitioners alike in the areas of automated reasoning, planning, (temporal) knowledge representation, and formal verification.
Download the slides from here.