2017/03/25 by Naveen Sundar Govindarajulu, Govindarajulu, Naveen Sundar, Selmer Bringsjord +1
Computer Science · #Computational Complexity (cs.CC) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Semantic Web and Ontologies #cs.CC #cs.LO
paper · pdf · doi:10.48550/arxiv.1703.08746
Short abstract presented at CiE 2014
arxiv created 2017/03/25 · openalex publication_date 2017/03/25 · arxiv updated 2017/03/28 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
The generally accepted wisdom in computational circles is that pure proof verification is a solved problem and that the computationally hard elements and fertile areas of study lie in proof discovery. This wisdom presumably does hold for conventional proof systems such as first-order logic with a standard proof calculus such as natural deduction or resolution. But this folk belief breaks down when we consider more user-friendly/powerful inference rules. One such rule is the restricted ω-rule, which is not even semi-decidable when added to a standard proof calculus of a nice theory. While presumably not a novel result, we feel that the hardness of proof verification is under-appreciated in most communities that deal with proofs. A proof-sketch follows.