15

I'm a computer science and philosophy double major. I know logic is paramount in computer science, but what about modal logic? Are there any practical applications in computer science and perhaps even outside of computer science?

Improve this question
15
  • Do applications in philosophy count?
    – J.P.
    May 18, 2015 at 16:44
  • What counts as practical? What for example counts as practical examples of normal logic?
    – Mozibur Ullah
    May 18, 2015 at 21:57
  • Humans do use a primitive form of modal logic in their speech and argument before it was formally formulated in the 20th century
    – Cicero
    May 19, 2015 at 4:55
  • @cicero: You might be interested to know that Aristotles books on logic - the organon - has a good introduction to the formal consideration of modal logic ie necessity and possibility and their inter-dependence.
    – Mozibur Ullah
    May 19, 2015 at 14:59
  • Interesting @MoziburUlla
    – Cicero
    May 19, 2015 at 15:00

7 Answers 7

Reset to default
5

A very practical application of modal logic is the control of traffic lights. Some approaches use fuzzy logic, but there are also Prior-Kripke based traffic lights.

Improve this answer
3

Model checking is an important application of modal logic in computer science. In model checking, you model a small piece of hardware or software as an automaton which deals with infinitely long words rather than finite words as in introductory textbooks. Various properties of the system can be expressed as those of the words accepted by the automaton. You regard infinite words as (linear) Kripke structures, and you can write the properties you want the system to have by formulas in temporal logic, a kind of modal logic. There are automatic procedures to test whether a given automaton accepts words that satisfy the properties expressed in that way.

Improve this answer
2

Godels incompleteness theorems has a long and complicated proof which can be made substantially simpler by making use of a modal logic, where the modality operator is interpreted as provability; this is an application in mathematics and logic.

Improve this answer
1
  • 1
    I think this is misleading. I what way does this reframing simplify the proof. You need to either independently prove Skolem's theorem, or do Godel numbering, even if you are interpreting modality this way. It may make it easier to state the propositions, but you still have to do all the same work.
    – user9166
    May 25, 2015 at 14:10
2

Modal logic captures meaning beyond clearly statable facts. It often reflects possibility, desirability, clarity, plausibility or some other sought goal (and simultaneously the restrictions on pursuing that goal), the kind of knowledge that someone has about what they are saying, that cannot be embedded meaningfully in the statement of the fact itself, but can only be alluded to.

You can think of the kinds of deductions made in expert systems as modal logic. "How possible and how definitive is each interpretation of the existing data? What additional information would the best interpretations make most relevant? So that is what I will ask next." is the standard step in a medical diagnosis system or a trend-recognition system.

But "Possible", "definitive", and "relevant" here, are modal concepts. They are about propositions. They limit reasonable interpretation without having much effect on the full range of interpretations. And they very hard to quantify or collect data on, or to combine given data about, reliably. So they call for something less that statistics and something more than formal logic.

Since goal-seeking systems that are not sheer numerical optimizations seem like a good way of addressing many problems with a computer, much of 'AI', from medical diagnosis simplification to good game character psychology, can be formulated as a rated modal logic.

The basic approaches to modal logic within philosophy do not get the right kind of attention to really develop into useful expert deduction systems. The intended semantics are different, and the common models immediately flee far from tractability. (Kripke semantics defies statistics in a big way.) But the ideas of modal logic do form the basis of interpreting subjectively-driven behavior and provide some of the motivations involved.

Improve this answer
2

Modal logic as usually developed formally following the work of C.I. Lewis is difficult to apply in computer science as well as practice , in large part because it is non-truth functional, and the truth table methods of ordinary classical logic do not work. It is possible to develop a truth-functional version based on the 3-valued logic of Lukasiewicz, but this is an unconventional and unfamiliar approach to the subject.

Improve this answer
7
  • Unfamiliar but familiar to you :-). Any references you suggest of reading this unconventional territory?
    – MathematicalPhysicist
    Nov 6, 2016 at 18:46
  • sapiencekb.com/3vml.htm
    – Confutus
    Nov 12, 2016 at 19:13
  • Do you have references for this article of yours? I hope I'll have time to read it tomorrow, it doesn't seem long though (so it makes me wonder :-) ).
    – MathematicalPhysicist
    Nov 12, 2016 at 20:02
  • OK, I read your article. Is this really something new and unfamiliar to logicians?
    – MathematicalPhysicist
    Nov 12, 2016 at 21:23
  • 1
    I had the same question, once. I found a lot of people who came close, but none who had put it all together. It's simple and obvious in hindsight, but the very devil to discover if you don't have the key.
    – Confutus
    Nov 13, 2016 at 9:43
2

Modal logic shares the same epistemological status as what Kant called "formal logic" in his first critique. That is to say, its internal consistency allows it to serve as a check against admitting certain propositions, or in the case of modal logic a measuring of certain models. But it is equally useless in determining what is either true or the best possible account in the actual world.

Improve this answer
1

According to the Stanford Encyclopedia of Philosophy, the answer is yes. One of the usages they cite is answering questions about decidability. Another is "bisimulation":

...Bisimulation provides a good example of the fruitful interactions that have been developed between modal logic and computer science. In computer science, labeled transition systems (LTSs) are commonly used to represent possible computation pathways during execution of a program. LTSs are generalizations of Kripke frames, consisting of a set W of states, and a collection of i-accessibility relations Ri, one for each computer process i. Intuitively, wRiw′ holds exactly when w′ is a state that results from applying the process i to state w.

The language of poly-modal or dynamic logic introduces a collection of modal operators □i, one for each program i (Harel, 1984). Then □iA states that sentence A holds in every result of applying i. So ideas like the correctness and successful termination of programs can be expressed in this language. Models for such a language are like Kripke models save that LTSs are used in place of frames. A bisimulation is a counterpart relation between states of two such models such that exactly the same propositional variables are true in counterpart states, and whenever world v is i-accessible from one of two counterpart states, then the other counterpart bears the i-accessibility relation to some counterpart of v. In short, the i-accessibility structure one can “see” from a given state mimics what one sees from a counterpart...

Garson, James, "Modal Logic", The Stanford Encyclopedia of Philosophy (Summer 2014 Edition), Edward N. Zalta (ed.), http://plato.stanford.edu/archives/sum2014/entries/logic-modal/.

Improve this answer

You must log in to answer this question.