Uniform Interpolation by Resolution in Modal Logic

Autor:	Jérôme Mengin, Andreas Herzig
Rok vydání:	2008
Předmět:	TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Negation normal form Computer science Normal modal logic Computer Science::Logic in Computer Science Multimodal logic Accessibility relation Modal μ-calculus Dynamic logic (modal logic) Modal logic Conjunctive normal form Algorithm
Zdroj:	Logics in Artificial Intelligence ISBN: 9783540878025 JELIA
DOI:	10.1007/978-3-540-87803-2_19
Popis:	The problem of computing a uniform interpolant of a given formula on a sublanguage is known in Artificial Intelligence as variable forgetting. In propositional logic, there are well known methods for performing variable forgetting. Variable forgetting is more involved in modal logics, because one must forget a variable not in one world, but in several worlds. It has been shown that modal logic K has the uniform interpolation property, and a method has recently been proposed for forgetting variables in a modal formula (of mu-calculus) given in disjunctive normal form. However, there are cases where information comes naturally in a more conjunctive form. In this paper, we propose a method, based on an extension of resolution to modal logics, to perform variable forgetting for formulae in conjunctive normal form, in the modal logic K.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::569e6ac651ada2efccc02d04bceec2f6 https://doi.org/10.1007/978-3-540-87803-2_19 Zobrazit plný text záznamu