- Submit
-
Browse
- All Categories
- Metaphysics and Epistemology
- Value Theory
- Science, Logic, and Mathematics
- Science, Logic, and Mathematics
- Logic and Philosophy of Logic
- Philosophy of Biology
- Philosophy of Cognitive Science
- Philosophy of Computing and Information
- Philosophy of Mathematics
- Philosophy of Physical Science
- Philosophy of Social Science
- Philosophy of Probability
- General Philosophy of Science
- Philosophy of Science, Misc
- History of Western Philosophy
- Philosophical Traditions
- Philosophy, Misc
- Other Academic Areas
- More
Switch to: References
Citations of:
Add citations
You must login to add citations.
|
|
|
We generalise an interval-related interpolation theorem about abstract-time Interval Temporal Logic, which was first obtained in [GUE 01]. The generalisation is based on the abstract-time variant of a projection operator in the Duration Calculus, which was introduced in [DAN 99] and later studied extensively in [GUE 02]. We propose a way to understand interpolation in the context of formal verification. We give an example showing that, unlike abstract-time ITL, DC does not have the Craig interpolation property in general, and establish (...) |
|
|
We present an embedding of quantified multimodal logics into simple type theory and prove its soundness and completeness. A correspondence between QKπ models for quantified multimodal logics and Henkin models is established and exploited. Our embedding supports the application of off-the-shelf higher-order theorem provers for reasoning within and about quantified multimodal logics. Moreover, it provides a starting point for further logic embeddings and their combinations in simple type theory. |
|
|
|
|
|
Quantified hybrid logic is quantified modal logic extended with apparatus for naming states and asserting that a formula is true at a named state. While interpolation and Beth's definability theorem fail in a number of well-known quantified modal logics , their counterparts in quantified hybrid logic have these properties. These are special cases of the main result of the paper: the quantified hybrid logic of any class of frames definable in the bounded fragment of first-order logic has the interpolation property, (...) |
|
|
A semantic embedding of quantified conditional logic in classical higher-order logic is utilized for reducing cut-elimination in the former logic to existing results for the latter logic. The presented embedding approach is adaptable to a wide range of other logics, for many of which cut-elimination is still open. However, special attention has to be payed to cut-simulation, which may render cut-elimination as a pointless criterion. |
|
|
|
|
|
|
PhilPapers logo by Andrea Andrews and Meghan Driscoll.
This site uses cookies and Google Analytics (see our terms & conditions for details regarding the privacy implications). Use of this site is subject to terms & conditions.
All rights reserved by The PhilPapers Foundation
Server: philpapers-web-6f9648bdd6-6d7m4 uwo