Questions tagged [modal-logic]
The modal-logic tag has no usage guidance.
21
questions
0
votes
0
answers
16
views
Is first order linear temporal logic a special case of first order modal logic?
Propositional linear temporal logic is a special case of propositional modal logic. Is first order linear temporal logic likewise a special case of first order modal logic?
- 237
1
vote
2
answers
59
views
What is the Kripke semantic for a linear temporal logic?
I've read that in general for a modal formula P, a world w and a Kripke frame ⟨W,R⟩
w⊨□P if and only if for every u∈W, if wRu then u⊢P
In case of LTL, being a modal logic, I assumed that the worlds ...
- 251
1
vote
1
answer
53
views
Why we can't use deduction theorem on soundness to contravene second incompleteness with lob's theorem
I'm starting to learn modal logic and there is something that's bothering my mind for a while.
we know from deduction theorem that $((\vdash q) \rightarrow (\vdash p)) \Leftrightarrow(\vdash (q \...
3
votes
1
answer
56
views
CTL trouble translating text into formula
I have an excercise where I have to translate verbally formulated statements into CTL formulas. I have particularly trouble with this one:
On every path q is true at least once and p was true ...
- 135
3
votes
1
answer
74
views
Uses of of the one-variable fragment of first-order logic aka S5
I'm looking at decidable fragments of first-order logic. It seems that FO(1), i.e. the one-variable fragment of first-order logic is equivalent to the modal logic S5. However, I cannot find a ...
- 448
3
votes
1
answer
342
views
How to understand quantifier without predication " ∀(λφ. (φ x m→ φ y))"?
I am reading about embedding/automation of modal logics in classical higher order logic (http://page.mi.fu-berlin.de/cbenzmueller/papers/C46.pdf) and Goedels proof of God's existence is prominent ...
- 1,381
3
votes
0
answers
49
views
$(\Box \forall x \varphi) \to (\forall x \Box \varphi)$?
I am working with a particularly forgiving interpretation of $\Box$ in Modal Predicate Logic. $M, w, g \models \Box \varphi$ iff for every $w' \in W$ such that $wRw'$, $M, w', g \models \varphi$ IF $\...
- 31
4
votes
2
answers
91
views
Euclidean Models
I am asked to prove that every Euclidean models satisfies $\diamond \diamond \diamond \varphi \to \diamond \diamond \varphi$. How can this be done? I don't see how it could even be true.
- 43
4
votes
2
answers
192
views
Meaning of the "why not" modality from linear type theory?
In linear type theory there is a modality written ! where !T can be read as "infinite copies of ...
- 341
2
votes
0
answers
26
views
Is it possible to define logic programming for every logic that has implication and conjunction connectives?
Is it possible to define logic programming for every logic that has implication and conjunction connectives? Does logic programming adds something new to the usual inference process. By usual ...
- 1,381
3
votes
0
answers
160
views
How to translate lambda calculus into (first-order, modal) logic, is it possible at all?
It is possible (using formal semantics) to translate natural language sentences into lambda expressions. So, is it possible to translate those lambda expressions into some logic, e.g. into first-order ...
- 1,381
4
votes
1
answer
168
views
How to express modalities in lambda calculus - are some extensions required?
Lambda calculus can be used for encoding semantics of natural language, e.g. http://yoavartzi.com/tutorial/ contains full details about semantic parsing of natural language: converting natural ...
- 1,381
2
votes
0
answers
58
views
How to express modalities in rule bases, knowledge bases or expert systems?
Knowledge bases and expert systems are usually production rules systems and as such they lack expressive means for expressing modalities like "agent believes in statement", "agent has duty to perform ...
- 1,381
0
votes
1
answer
226
views
How to represent software code for code generation / automatic programming? How to integrate procedural and declarative knowledge?
I am learning about deontic logics and there I can make the following inferences: If A then there is **duty to create an entity of class C**, ...
- 1,381
2
votes
1
answer
119
views
Modal Logic - □ distribution over →
In the modal logic K does □ distribution over →?
For example, would the following be correct?
□(p → q) ≡ □p → □q
- 264
6
votes
1
answer
486
views
Kripke Models - evaluating the meaning of $\Box\Box p$
In Kripke models the evaluation of $x \vdash \Box p$ would be that every world reachable from $x$ satisfies $p$.
But how would the truth of $\Box\Box p$ be evaluated in Kripke models?
- 264
3
votes
1
answer
478
views
Modal logic axiom S4, transitive and reflexive frame, tableaux solver
I have a difficult problem to solve which as mentioned in the title is related to modal logic axiom S4.
So, here is some background knowledge that can be useful:
S4 axiom is a class of transitive and ...
- 137
3
votes
1
answer
136
views
complexity of modal logic axioms
I am writing a paper in which I want to include complexity results for different modal logics and possibly add a reference to a specific paper.
At the moment I have the following:
K- no restrictions ...
- 31
2
votes
2
answers
3k
views
The use of modal logic in computer science [closed]
I have a tentative understanding of modal logic. Can anyone explain modal logic as it is used in computer science?
- 131
1
vote
1
answer
469
views
Intuitive meaning of modal $\mu$-calculus formula
I am solving one of the past exams and I am not certain with my solution to one of the exercises. The exercise is asking to give intuitive meaning to modal $\mu$-calculus formula:
$$ \phi = \mu Z. \...
- 253
3
votes
3
answers
395
views
Why is GFp -> GFq false in LTL, even though GFp and GFq are false?
Consider the Kripke structure:
$$
\begin{array}{ccccccc}
\to & (p, \neg q) & \to & (\neg p, \neg q) & \to & (\neg p, q) \\
& \circlearrowright & & \circlearrowright ...
- 31