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?

Chris Sunami
  • 25,314
  • 1
  • 44
  • 82
  • Do applications in philosophy count? – J.P. May 18 '15 at 16:44
  • What counts as practical? What for example counts as practical examples of normal logic? – Mozibur Ullah May 18 '15 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 '15 at 04: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 '15 at 14:59
  • Interesting @MoziburUlla – Cicero May 19 '15 at 15:00
  • There are apparently applications in computer circuit design -- nothing that can't be done in ordinary true-or-false logic, but, for some applications, significant savings in numbers of components can be achieved. See "multi-valued logic gates". – Dan Christensen May 19 '15 at 15:18
  • @DanChristensen I would not consider polyalethian logic (the ability to take ambiguous truth values that are nonetheless meaningful) to be modal logic. They often go together because evaluating the acceptability of contradictions is a part of deontology, but when applied directly, statistics is not a modality. –  May 19 '15 at 15:57
  • @jobermark There is nothing ambiguous about these circuits. Instead of restricting output values to only two distinct voltages (for 0 or 1), there may be, say, 8 levels. (Not sure about the technical details.) – Dan Christensen May 19 '15 at 16:05
  • @DanChristensen I just meant non-true, non-false. That puts this even further into the multivalued camp and even farther outside modal logic. Statistics rounded to eight values are still statistics, (quintiles and all that.) –  May 19 '15 at 16:20
  • @jobermark I doubt that it would be used for statistics. More likely en-coding digital data, e.g. text and graphics. My point was, all of this can be achieved using only ordinary true-or-false data as well. – Dan Christensen May 19 '15 at 16:26
  • @DanChristensen 1) Whatever uses advanced logics have they will always be doable in ordinary true-and-false data as well. All Turing Machines are created equal. 2) I am not talking about applications to statistics, but of statistics. Combining electrical signals in any non-binary way is always going to be statistical, electrons exist in large numbers and you decide a voltage by counting them. I think we have different notions of 'statistics' in mind. 3) The general point is this stuff may be more interesting than this question, but it is not part of this question. –  May 19 '15 at 16:53
  • @jobermark The physical implementation is immaterial here. This has nothing to do with statistics. The point is (1) there are practical applications of multi-value logic (3+), and (2) these applications can also be done using ordinary logic. – Dan Christensen May 19 '15 at 17:50
  • @DanChristensen But the question is not about multivalued logic! I am sick of repeating myself. I already totally agreed with 1 and 2 and granted that we have different notions of what statistical means in this context. I understand yours, it is not the only one. Listen or stop speaking. My 1 implies your 2. My 3 points out that your 1 is completely true, but off-topic. When someone actually agrees with you, and they say so quite clearly, and you can't tell, you are not listening. –  May 19 '15 at 18:36
  • Interestingly enough, on the back of my modal logic book it lists the categories the book falls under - computer science is listed. – SteenJobs May 21 '15 at 21:34
  • Why come back after a year and edit this into a different question? Just ask a new question. It's OK if it's similar, the new version has a different emphasis. – Chris Sunami Mar 03 '17 at 02:08

7 Answers7

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.

paschep
  • 136
  • 1
  • 3
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.

Pteromys
  • 201
  • 1
  • 2
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.

Mozibur Ullah
  • 1
  • 14
  • 88
  • 234
  • 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. –  May 25 '15 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.

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.

Confutus
  • 574
  • 2
  • 9
  • Unfamiliar but familiar to you :-). Any references you suggest of reading this unconventional territory? – MathematicalPhysicist Nov 06 '16 at 18:46
  • http://sapiencekb.com/3vml.htm – Confutus Nov 12 '16 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 '16 at 20:02
  • OK, I read your article. Is this really something new and unfamiliar to logicians? – MathematicalPhysicist Nov 12 '16 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 '16 at 09:43
  • So perhaps you can publish this article in some peer review journal; though if you say that Lukasewicz found it already I am pretty sure it is familiar to people in logic. (Maybe it's ancient also, before Lukasewicz). Where did you find it covered? perhaps the handbooks of philosophical logic by Dov Gabbay et al? – MathematicalPhysicist Nov 13 '16 at 12:42
  • Lukasiewicz didn't go so far as to apply his "definite" operator to his conditional: This is the key missing piece in making his logic full-featured. Of the works cited in the SEP article on Multivalued logic, http://plato.stanford.edu/entries/logic-manyvalued/ I consulted; Ackermann; Bolc and Borowic; Malinowski; and Rescher. None of them mention this, either. – Confutus Nov 13 '16 at 20:24
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.

Bernie Freydberg
  • 21
  • 1
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/.

Community
  • 1
Chris Sunami
  • 25,314
  • 1
  • 44
  • 82