8
$\begingroup$

I heard theorem proving is a hard problem, hard enough that it contributed to an early AI winter. But how hard?

While reading about proof assistants, I have come to realize that there are many types of theorem proving/logic behind: propositional logic, first-order (FOL), high-order (HOL), various type theories, and many others maybe.

My question is:

What are the computational complexity (roughly speaking) for theorem proving for the different types of logic behind theorem provers?

(e.g. undecidable, NP-hard, polynomial time etc.)

I just wanted to get a rough idea.

Improve this question
$\endgroup$
2
  • 2
    $\begingroup$ Basically, being undecidable is a necessary condition for it to be interesting. $\endgroup$
    – Trebor ♦
    Feb 19, 2022 at 6:09
  • 1
    $\begingroup$ Propositional calculus is a semi-exception, because it is so foundational. But it also have undecidable variants like full linear logic. Other decidable theories like highschool geometry is only of interest to algorithm optimization, not to geometry. $\endgroup$
    – Trebor ♦
    Feb 19, 2022 at 6:13

2 Answers 2

Reset to default
10
$\begingroup$

Briefly:

Propositional logic: determining whether there is a proof is $\mathsf{NP}$-hard, since proving a formula entails determining that its negation is not satisfiable.

First-order logic: determining whether a proof exists is undecidable (Gödel's theorem).

Type theory: should also be undecidable since we can embed first-order logic in type theory.

Improve this answer
$\endgroup$
7
  • 1
    $\begingroup$ Nice Answer! Small addition: you can also find NP-hard task in built-in DNF solver for cubical subsystems in cubical type checkers. $\endgroup$
    – Namdak Tönpa
    Feb 21, 2022 at 16:58
  • 1
    $\begingroup$ If I'm not mistaken, it should be Church's theorem (1936), not Gödel's theorem (1931). $\endgroup$
    – M. Lonardi
    Feb 21, 2022 at 23:49
  • $\begingroup$ @M.Lonardi Church's Corollary 😏 $\endgroup$
    – Bjørn Kjos-Hanssen
    Feb 22, 2022 at 2:52
  • $\begingroup$ @NamdakTönpa interesting, does that DNF solver get used a lot? $\endgroup$
    – Bjørn Kjos-Hanssen
    Feb 22, 2022 at 3:43
  • $\begingroup$ E.g. with multidimensional cubes. $\endgroup$
    – Namdak Tönpa
    Feb 22, 2022 at 5:11
7
$\begingroup$

As an addition: proof checking (rather than search) already can be very hard. For instance, proof checking in type theory relies on conversion checking, which itself needs to evaluate arbitrary functions definable in the system. In something as expressive as CIC, this in theory has an extremely high complexity. In fact, one of the biggest known integer (Loader’s number) is linked to the size of functions definable in the Calculus of Constructions.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.