it is well-known that propositional logic problems such as

$$ (p\leftrightarrow q) \lor r \quad\overset{?}{\vdash}\quad (((p\lor q)\to(p\land q)) \land \lnot r)\lor r$$

can be simply solved by evaluating the corresponding boolean functions for the $2^n$ possible values of the $n$ boolean variables (here $p,q,r$).

my question is then : instead of hand-writing such a propositional logic solver, couldn't we search for a program capable of generating such a solver ?

what would be then the minimal core / set of concepts and rules needed for a program being capable of ''discovering'' and ''solving'' the propositional calculus ?

is it a unsolvable artificial intelligence problem, or would it have some nice solutions, helpful for solving the more interesting higher order logics ?

  • 2
    $\begingroup$ No, this is not how artificial intelligence works. $\endgroup$ Feb 26, 2016 at 10:17
  • $\begingroup$ @YuvalFilmus : do you have some precision on your comment, or is it only a general statement that what we call "AI" is until now more about statistical machine learning than artificial intelligence ? $\endgroup$
    – reuns
    Mar 30, 2016 at 14:27
  • $\begingroup$ What you describe is at the moment very much out of reach. It's more like science fiction. $\endgroup$ Mar 30, 2016 at 15:15
  • $\begingroup$ @YuvalFilmus : you know that solving the propositional calculus is really not complicated, and that the automatic theorem provers can solve some quite complicated problems, hence I don't think it is out of reach, it is just that we don't know yet how to do it, but it doesn't have to be so complicated compared to what we already do $\endgroup$
    – reuns
    Mar 30, 2016 at 15:37
  • $\begingroup$ I think to it as one of the simplest possible meta-maths problems, and as a first (small) step toward a mathematician AI $\endgroup$
    – reuns
    Mar 30, 2016 at 15:40

1 Answer 1


If there are no quantifiers, testing validity of such formulas is equivalent to testing satisfiability of the complement of the formula. That can be done with a SAT solver. SAT solvers and the satisfiability problem are well-studied. So, the minimal set of concepts needed would be: enough to solve SAT.

Statements with quantifiers are harder (QBF). Higher-order logics are harder still.

  • $\begingroup$ I don't see how SAT problems which are $$\exists x_1,\ldots,x_n \quad P(x_1,\ldots,x_n)$$ (so they are $1$st order logic, not propositional logic) are related to my question which is about how generating automatically an algorithm for solving propositional calculus problems $\endgroup$
    – reuns
    Feb 26, 2016 at 8:34
  • $\begingroup$ in fact, SAT solvers are much more than that : they take in account the time and space complexity needed to solve the $\exists x, P(x)$ problem, and try to generate an algorithm for solving it as fast as possible. whereas what I meant in my question is generating a simple propositional logic solver, which doesn't care of how much time will be needed, as far as it is finite (so testing the $2^n$ possible values of $x$ is not a problem), do you see what I mean ? $\endgroup$
    – reuns
    Feb 26, 2016 at 8:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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