Background: M.S. in C.S. and A.I.Positive Points
1. The MIT Press is putting out texts on formal logic
2. Dynamic Logic has all the building blocks to reason formally
about computer algorithms
3. The book shows how extensions of logic (such as modal, or
temporal) can be built on a foundation of formal logic.
How shall I say this? I am still shocked within the circles of
software engineering, to run into Masters degrees who don't even
know one complete notation system for formal logic. The ability
to produce formal proofs of validity, is a very basic ability
for a programmer creating complex algorithms. The European Union
seems a little bit ahead of North American programmers, in this
respect.
And programmers who do not know any notations of formal logic,
probably will never have studied computer algorithms for
automated reasoning. (And will probably be abysmally ignorant
of the classes of intractable problems associated with automated
reasoning.)
The situation among "hard" engineers (as opposed to software
engineers) seems to be worse (which is why I laud MIT putting
out introductory books on logic). Almost every week I run into
engineers who cannot understand that formal logic and mathematics
are not the same thing. More precisely, that one can have a
complete, valid, consistent system of logic, without a number
system.
I am happy that the big engineering schools are becoming
conscious that an ignorance of formal logic is a serious flaw
in hard and soft engineers. The next difficulty follows logically:
engineers discover the power of formal logic to
reason about reality far beyond what can be accurately described
by analytic mathematical methods (currently). And they want to
immediately implement automated reasoning software, without
knowing anything about the nature of THAT problem. We need more
books on software algorithms, for extensions of formal logic.
And that is NOT this book. This book is an appetizer.
