Ben Brink wrote: > > Jon, > > Using deMorgan's Law, statement should be equivalent > to (~p ^ ~q) v (~p ^ q). If I'm not mistaken, there's > a "distributive" law which says this is equivalent to > ~p ^ (q v ~q). This last should be equivalent to ~p. > To me this is easier than the graphs. > > Ben
But it would be necessary to write out all the steps in order to have a fair comparison of prove complexity.
This formulation of logical graphs is based on the work that C.S. Peirce (1839-1914) did on various systems of graphical logics. These ideas were revived again in the late 60's by George Spencer Brown, who wrote a book called ''Laws of Form''. They also formed the basis of John Sowa's "Conceptual Graphs", which remain under active development to this day.
When I began working on computerized theorem proving in the late 1970's I quickly discovered that the formulation given here was especially well suited to computational methods. One reason for this is that everything is based on only four basic axioms, which greatly reduced the amount of "creativity" that is demanded of the theorem prover. Another reason is that it's possible to establish a Case Analysis-Synthesis Theorem (CAST) that allows one to check logical equivalence in a very routine manner, roughly analogous to truth tables but much more efficient and flexible.
Of course, having to draw the logical graphs in ASCII graphics is pretty klunky -- they are much quicker to sketch free hand and they are even better suited to the construction of graph theoretic data structures in computer memory.
Feel free to use the talk page of that wiki article if you have any questions, as I will probably be trying to make the presentation there a little clearer.