|
Hi there,
I've recently reread the (updated) paper of Martin
Muller about Proof Set Search(http://www.cs.ualberta.ca/~mmueller/publications.html),
and also had a look to the paper of Martin Schijf (http://hoggy.virtualave.net/y.bishop/page1.htm),
about using PN Search with transpositions.
Martin Muller claims that Shijf's algorihtm is too
expensive (memory and time), and Schijf says the same thing about his so called
"theoritical" algorithm (for DAG).
However Schijf also describes a "practical"
algorithm and reports experimentation that show the superiority of the practical
algorithm. Unfortunately the "practical" algorithm is only described in a few
words, and it is not obvious (at least for me) if it works, how it works, and if
it is strictly equivalent to the "theoritical" algorithm. That is if it really
computes the correct PN, or only an approximation that is better on the average
than the standard PN algorithm.
Did somebody had a closer look at this, and have
any idea about how this "practical" algorithm works, and if yes how it compares
to PSS?
Antoine.
|