3 ms·
This sounds to me like what we now call the Busy Beaver problem. http://en.wikipedia.org/wiki/Busy_beaver http://en.wikipedia.org/wiki/Busy_beaver
by thisisnotmyname 16y ago
This sounds to me like what we now call the Busy Beaver problem. http://en.wikipedia.org/wiki/Busy_beaver http://en.wikipedia.org/wiki/Busy_beaver
- bdr 16y agoIt's not. Godel is asking, what's the fastest program that can tell if a (first order predicate logic) formula is provable? Maybe you were confused by the 'max', but what he's doing is defining the complexity of the prover by the hardest (max computational time) formula instance for each length n. You still try to handle that maximum difficulty case as efficiently as possible, it just happens to take the longest.