Deduction versus Reduction

In my last post, Software Verification, I criticized the field’s heavy reliance of theorem provers based on predicate logic. I mentioned some obvious problems such as exponential proof procedures, but a Coverity presentation “Selling an Idea or a Product” pointed me to other nonobvious problems. A slide (#17) titled “Myth: more analysis is always better” hinted that more analysis does not always improve results; it can sometimes produce worse results.

• Ease of Diagnosis – The longer the chain of reasoning, the harder the bug is to reason about, since the user has to manually emulate each step, but, unfortunately, long chains of reasoning are also needed to find some high-level bugs.
  
  Another related example is the Simplify theorem prover, which can determine if linear arithmetic constraints are contradictory using the Simplex Method. However, such a general procedure may not be very advantageous, since people will typically write simple inequalities that they can easily reason about. A general analysis consumes more resources than a narrow solver. Secondly, a human being may not be able to understand a complicated error (an empty intersection of several inequalities) reported by the Simplex solver and simply dismiss it as a false positive. Once again, such errors are not likely, because humans do not typically write such code in the first place. [I believe that the Simplify prover actually uses a more optimized algorithm, Nelson-Oppen, for simple inequalities.]
  
• False Errors – The greater the number of steps, the more likely that the analysis contains an error. If there is false information in the knowledge base, then any assertion can be proved via a refutation-based proof procedure.

The alternative to logical deduction is functional reduction in which expressions are continually reduced to normal forms, so that equivalent expressions will eventually look the same. In other words, algebra not logic. The benefit is greater efficiency due to the elimination of much nondeterminism, deeper inferences, and more opportunities for dynamic programming to tame the unwieldy beast. This approach is also referred to as equational logic and is very similar to high-school algebraic proofs.

Last year I wrote a post, On Intelligence, which is relevant to this post. In it, I quote the words of Stephen Wolfram, on the subject of logic and rules…

But what about capabilities like logical reasoning? Do these perhaps correspond to a higher-level of human thinking?

In the past it was often thought that logical might be an appropriate idealization for all of human thinking. And largely as a result of this, practical computer systems have always treated logic as something quite fundamental. But it is my strong suspicion that in fact logic is very far from fundamental, particularly in human thinking.

For among other things, whereas in the process of thinking we routinely manage to retrieve remarkable connections almost instantaneously from memory, we tend to be able to carry out logical reasoning only by laboriously going from one step to the next. And my strong suspicions is that when we do this we are in effect again just using memory and retrieving patterns of logical argument that we have learned from experience.

The primacy of reduction rules (patterns stored in memory) over logical inference in human thought shouldn’t be surprising given the efficiency of the former; the latter is equally as “laborious” for humans as it is for computers.

Comments

[Wesner Moise]

The best illustration of my post are OBDDs (Ordered Binary Decision Diagrams). These are canonical if-then-expressions, which outperform by a factor of 1000 more traditional techniques in theorem proving.

http://citeseer.ist.psu.edu/cache/papers/cs/1068/http:zSzzSzwww.cs.utexas.eduzSzuserszSzmoorezSzpublicationszSzbdd.pdf/moore92introduction.pdf

[yalin]

Hello,

Nstatic is a free soft ou no?

where can'i download it?
Tanks