# a program discovering himself how to solve propositional calculus

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 ?

• No, this is not how artificial intelligence works. Feb 26, 2016 at 10:17
• @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 ? Mar 30, 2016 at 14:27
• What you describe is at the moment very much out of reach. It's more like science fiction. Mar 30, 2016 at 15:15
• @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 Mar 30, 2016 at 15:37
• I think to it as one of the simplest possible meta-maths problems, and as a first (small) step toward a mathematician AI Mar 30, 2016 at 15:40

• 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 Feb 26, 2016 at 8:34
• 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 ? Feb 26, 2016 at 8:54