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 ?
a program discovering himself how to solve propositional calculus
artificial intelligence;first order logic;propositional logic