Talk:Dynamic logic (modal logic)

Fuzzy logic is the same as dynamic logic?

I would like to see some evidence for the claim that Fuzzy logic is the same a Dynamic logic. While Fuzzy logic is a fairly well-defined topic (http://www-2.cs.cmu.edu/Groups/AI/html/faqs/ai/fuzzy/part1/faq.html ), dynamic logic doesn't seem to be a fixed term at all (my Google impression). AxelBoldt 21:53 Jan 4, 2003 (UTC)

I have never saw any claim that fuzzy logic is equivalent to dinamyc logic, whatever is dynamic logic. Therefore, I believe this page should be considered a personnal view of the matter and not the accepted standard of the term. I will take the responsability to initiate a refactoring, at least not redirecting Fuzzy logic to Dynamic logic. User: Geraldo Xexéo

I have now found what does dynamic logic means, and have nothing to do with fuzzy logic. Cited directly from the article: DL is a multi-model logic with a a possible worlds semantic, which distinguishes between expressions of two sorts: formulae and programs. What does it has to do with Fuzzy Logic???? User: Geraldo Xexéo

I agree with both opinions, fuzzy logic is another thing. Perhaps the author is confused with some uses of fuzzy logic and ignores what is dynamic logic. Dynamic Logic is a symbolic logic related to proccesses, with rules like $[\alpha ]p\wedge q=>[\alpha ]p\wedge [\alpha ]q$ where $\alpha$ is a process $p\wedge q$ is a contition to meet after the processess between squared brackets (in this example just $\alpha$) finish. In this sense dynamic logic is considered a kind of modal logic, comparing the processes with modal operators. At this time I do not know more about the subject, but I am shure it is not fuzzy logic!

What the heck is this?

OK, I have to admit I have no idea what this article is talking about. (Though regarding comments about fuzzy logic, I can say it doesn't seem to be like it at all.) We need some more about the implications of this and how it's applied and all that. Something like "The key idea is that programs can be represented by means of an algebra of actions, each of whose elements determine two dual modalities: action a gives a 'box' modality [a], and a diamond modality <a>" reads to me like, "gibber gibber gibber blah algebra blah gibber gibber [a] gibber <a>". :) - Furrykef 00:01, 10 Nov 2004 (UTC)

I rewrote the article:it's not exactly didactically ideal, but at least it's correct, where what I replaced was mostly nonsense. All references to fuzzy logic were deleted. I might try and improve it, but it's far from an editing priority for me. ---- Charles Stewart 00:58, 10 Nov 2004 (UTC)

Unfortunately, I still have no idea what it really is. :) - Furrykef 00:01, 12 Nov 2004 (UTC)

Right, but at least you don't believe it to be something other than what it is. OK, I've put it on my reminders list, so I will get around to it eventually. ---- Charles Stewart 09:37, 12 Nov 2004 (UTC)

Now that a year has passed I've taken the liberty of expanding it to an article. Please feel free to make improvements as you see fit. -- Vaughan Pratt 05:56, 6 November 2005 (UTC)

Rename this page something else

I've been working in Silicon Valley in the field of logic and circuit design, for CPUs and later, ASICs, since 1992. I've talked with people on at least seven different full-custom CPU design teams. I've never head anyone refer to dynamic logic (as it relates to circuits) as "clocked logic". I may have seen this usage in the literature, however. Didn't Svennson refer to his latches as "clocked CMOS"?

I think "Clocked logic" is pretty nonstandard, and "dynamic logic" would be better used as the title of the page relating to circuit design. Furthermore, my guess is that there are at least thousands of circuit designers who are familiar with the term "dynamic logic" as it relates to circuits, and use it at least once a month. (Basis: there are at least 3000 people at ISSCC every year, many more that can't go for various reasons, and everyone I've talked to there knows what dynamic logic is at it applies to circuits.) I highly doubt there are anywhere near that many researchers in AI who use the phrase "dynamic logic"... there's just not enough economic activity there to pay all those people.

So I think this "clocked logic" article should be renamed "dynamic logic", and this article currently at "dynamic logic" should be renamed something else again.

But I don't know what to rename this article. Maybe "Dynamic logic (AI)". Iain McClatchie 6 July 2005 03:20 (UTC)

To get a more quantitative idea of how the term "Dynamic Logic" is used in the real world, why not type it (in double quotes) to Google? I tried this and found that of the first 40 hits, 20 of them were to the meaning used in the article. A number of hits referred to companies with that name, one in West Lothian doing monitoring and control, another in the advertising business. The remaining few referred to digital circuits. Although AI is one area in which dynamic logic has been applied, it was originally intended as a logic for program verification, and the recent book "Dynamic Logic" by Harel, Kozen, and Tiuryn brings that perspective to the subject. Vaughan Pratt 23:07, 5 November 2005 (UTC)

You're right. There are far more references to this non-circuit-design dynamic logic. I still doubt the mathematical idea is more common among people than the circuit design idea, but the math folks have won the 'net. Now I think the "clocked logic" article should be renamed "dynamic logic (circuit design)", and that this "dynamic logic" article should be renamed "dynamic logic (mathematics)". Iain McClatchie 00:18, 6 November 2005 (UTC)

I took the liberty to rename this page - I'll also rename clocked logic to "dynamic logic (digital logic)". I hope noone gets pissed. Fresheneesz 20:46, 5 March 2006 (UTC)

2006 cut & paste move

[1] Needs fixing to attribute earlier edits [2]. Tijfo098 (talk) 14:57, 28 April 2011 (UTC)

It was fixed by admin User:CBM. Tijfo098 (talk) 21:16, 29 April 2011 (UTC)

Possibly fallacious remark about random assignment

At the end of the Remark in the random assignment section, it is stated as a fact (based on a "proof" by Dijkstra) that the random assignment program x:=? is impossible. The considerable discussion in the article Unbounded nondeterminism gives various frameworks (Turing machines, actors, etc.) in which the question of its impossibility could be decided either way.

When the framework is dynamic logic itself, if the type of x is a finite domain (e.g. Bool, or more generally the integers mod 2ⁿ for some natural number n) the impossibility argument clearly fails. If on the other hand x is of type Nat, i.e. arbitrary precision, then the dynamic logic program x:=0; (x:=x+1)* implements x:=? (though not if x is of type Int). The alleged impossibility of the program x:=? for any infinite domain then entails the impossibility of *, since x:=0 and x:=x+1 are surely possible. Comments?

(As the inventor of x:=? [1976] I prefer to recuse myself from judgment on that question. Clinger's point at the end of the section Unbounded_nondeterminism#Arguments_for_dealing_with_unbounded_nondeterminism, about what might be more clearly stated as the possibility of a finitely-branching tree with infinitely many leaves all finitely far from the root, bears on this. Dijkstra's "proof" would appear to have overlooked this possibility.) Vaughan Pratt (talk) 20:40, 27 April 2016 (UTC)

I've changed this remark to the paragraph "Dijkstra claimed to show the impossibility of a program that sets the value of variable x to an arbitrary positive integer.[1] However, in dynamic logic with assignment and the * operator, x can be set to an arbitrary postive integer with the dynamic logic program $a\equiv x:=0;(x:=x+1)*$: hence we must either reject Dijkstra's argument or hold that the * operator is not effective." — Charles Stewart (talk) 12:05, 29 April 2016 (UTC)

Minor inconsistency in syntax

In the axiom section, we read "the two inference rules modus ponens ($\vdash p$ and ${\displaystyle \vdash p\to q}$ implies ${\displaystyle \vdash q\,}$) and necessitation ($\vdash p$ implies ${\displaystyle \vdash [a]p\,}$)," and in the derived rules section, we see the notation "$b\to [k]b\vdash b\to [k*]b\,\!$". If I'm not mistaken, "$\vdash p$ implies $\vdash q$" and "$p\vdash q$" mean the same thing, but I confess I puzzled over the two distinct expressions. It would be nice if we settled on one or the other throughout the article.

I won't make the change because I have the nagging feeling that maybe there's a difference between the two statements that I'm not getting. Phiwum (talk) 23:21, 10 December 2019 (UTC)

I'm also confused. In the usual sequent calculus, $p\vdash q$ implies $\vdash p\to q$. But that doesn't hold here? Taral (talk) 23:58, 2 May 2020 (UTC)