2014/11/12 by Pavel Pudlák, Pudlak, Pavel · 1 citation
Computer Science · #03D15 #Artificial Intelligence in Games #Computability, Logic, AI Algorithms #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Machine Learning and Algorithms #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1411.3304
openalex publication_date 2014/11/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Suppose that \Φ is a consistent sentence. Then there is no Herbrand proof\nof \¬ \Φ, which means that any Herbrand disjunction made from the prenex\nform of \¬ \Φ is falsifiable. We show that the problem of finding such a\nfalsifying assignment is hard in the following sense. For every total\npolynomial search problem R, there exists a consistent \Φ such that\nfinding solutions to R can be reduced to finding a falsifying assignment to\nan Herbrand disjunction made from \¬ \Φ. It has been conjectured that\nthere are no complete total polynomial search problems. If this conjecture is\ntrue, then for every consistent sentence \Φ, there exists a consistence\nsentence \Ψ, such that the search problem associated with \Ψ cannot be\nreduced to the search problem associated with \Φ.\n