I suspect that it should be the same as that of the Turing machine halting problem, which wikipedia gives as GenP and attributes this result to Hamkins and Miasnikov, but I am not sure. Is the generic complexity of FOPC equal to that of TMs? For instance, the Turing machine with two way infinite tape is apparently not known to be equivalent to the TM with one way tape. That is one of the things that make me worry I don't really understand what is going on. If FOPC is in GenP, I would expect there to be solvers/provers for FOPC which input any well formed formula, and return true, false, or undecided in polynomial time and correctly decide most questions. Does this apply to Otter, Prover9 and similar systems?
4
-
$\begingroup$ I guess most of the people here, myself included, have no idea about generic complexity. Care to elaborate? $\endgroup$– Dima PasechnikCommented May 26, 2014 at 0:08
-
$\begingroup$ Wikipedia Generic-case complexity is a good start. Three other references: homepages.ecs.vuw.ac.nz/~downey/generic_decision.pdf arxiv.org/abs/math/0504351 omskconf2009.oscsbras.ru/miasnikov2.pdf $\endgroup$– Jim GraberCommented May 26, 2014 at 13:08
-
$\begingroup$ A translation of this reference might be very informative: mathnet.ru/php/… $\endgroup$– Jim GraberCommented May 26, 2014 at 13:09
-
$\begingroup$ +1. I like this question very much. But it seems likely that the answer will depend on the details of the syntactic formalism. For example, insisting on normal forms or changing which logical connectives are allowed could conceivably affect the density of the set of validities. Also, adding extra predicate, function and constant symbols will affect density. $\endgroup$– Joel David HamkinsCommented Jun 2, 2014 at 13:05
Add a comment
|