Jon Awbrey
Registered: Feb 2004
Posts: 558 
RISCy Theorem Proving
Kovas,
I ran into a similar problem when I was just
beginning to write theorem proving programs.
For example, there are axiom systems for
propositional logic that use umpteen
axioms, some that use eight, and some,
like the one that comes down to us
from C.S. Peirce and Spencer Brown,
that uses only four initial axioms.
There might be additional oomph in
the more complicated axiom, but
the overhead bottleneck comes
at the point where you have
to decide which axiom to
use to advance a proof,
and many times you are
reduced to trying each
of them at random, so
the degree of the
branch point is
the critical
factor.
Jon Awbrey
Report this post to a moderator  IP: Logged
