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.

$\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

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.

$\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$ 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$ Feb 22, 2022 at 2:52
  • $\begingroup$ @NamdakTönpa interesting, does that DNF solver get used a lot? $\endgroup$ Feb 22, 2022 at 3:43
  • $\begingroup$ E.g. with multidimensional cubes. $\endgroup$ 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.

$\endgroup$

Your Answer

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

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