0
$\begingroup$

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 ?

Improve this question
$\endgroup$
15
  • 2
    $\begingroup$ No, this is not how artificial intelligence works. $\endgroup$
    – Yuval Filmus
    Commented 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
    Commented 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$
    – Yuval Filmus
    Commented 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
    Commented 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
    Commented Mar 30, 2016 at 15:40

2 Answers 2

Reset to default
2
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • $\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
    Commented 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
    Commented Feb 26, 2016 at 8:54
0
$\begingroup$

I'm not quite sure how you would define success, but here are a couple of references and some context to help you get started.

Have a look at this paper in the AI Journal:

A computational approach to George Boole’s discovery of Mathematical Logic

The underlying approach to be seems to be an old-fashioned production system.

I would be remiss if I didn't mention the now ancient Automated Mathematician program by Lenat. The Wikipedia article gives a good overview of the program as well as its considerable shortcomings. Nice related references there as well.

Finally, here's a recent New York Times article that might be relevant.

Improve this answer
$\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.