A variant of Beth's tableaux method for polymodal logics
Jeudi 2 octobre 2003 à 14 heures
Salle des thèses de l' Irit
Résumé : A variant of Beth's tableaux method for polymodal languages is considered. The main idea is to propose an algorithm which for a given formula return either a tree like Kripke model such that in the root this formula is true or a proof of its negation. In this way we obtain a constructive proof of decidability and completeness for simple modal logics.
Retour à la page
des séminaires