- Craig interpolation for linear temporal languages
- Lecture Notes in Computer Science
- Pages (from-to)
- Document type
- Faculty of Science (FNWI)
Interfacultary Research Institutes
- Informatics Institute (IVI)
Institute for Logic, Language and Computation (ILLC)
We study Craig interpolation for fragments and extensions of propositional linear temporal logic (PLTL). We consider various fragments of PLTLobtained by restricting the set of temporal connectives and, for each of these fragments, we identify its smallest extension that has Craig interpolation. Depending on the underlying set of temporal operators, this extension turns out to be one of the following three logics: the fragment of PLTLhaving only the Next operator; the extension of PLTLwith a fixpoint operator μ (known as linear time μ-calculus); the fixpoint extension of the "Until-only" fragment of PLTL.
- go to publisher's site
- Proceedings title: Computer Science Logic: 23rd International Workshop, CSL 2009, 18th Annual Conference of the EACSL, Coimbra,
Portugal, September 7-11, 2009: proceedings
Place of publication: Berlin
Editors: E. Grädel, R. Kahle
If you believe that digital publication of certain material infringes any of your rights or (privacy) interests, please let the Library know, stating your reasons. In case of a legitimate complaint, the Library will make the material inaccessible and/or remove it from the website. Please Ask the Library, or send a letter to: Library of the University of Amsterdam, Secretariat, Singel 425, 1012 WP Amsterdam, The Netherlands. You will be contacted as soon as possible.