Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [modal-logic]

The tag has no usage guidance.

3
votes
1answer
44 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 ...
3
votes
0answers
55 views

Finiteness of the set of equivalence classes of formulas generated by boolean combination

Define a relation $\equiv$ on the set of modal formulas by $\phi \equiv \psi \Leftrightarrow (\forall M\forall w, M,w \models \phi\Leftrightarrow M,w \models \psi)$ (so it is an equivalence relation) ...
1
vote
0answers
22 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 ...
3
votes
0answers
78 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 ...
4
votes
1answer
74 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 ...
3
votes
0answers
43 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 ...
0
votes
1answer
124 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
votes
1answer
79 views

Modal Logic - □ distribution over →

In the modal logic K does □ distribution over →? For example, would the following be correct? □(p → q) ≡ □p → □q
5
votes
1answer
174 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?
3
votes
1answer
307 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 ...
2
votes
1answer
106 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 ...
1
vote
2answers
1k 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?
1
vote
1answer
369 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. \...
3
votes
3answers
242 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 ...