1
$\begingroup$

When will it be possible to give a computer program a bunch of assumptions and ask it if a certain statement is true or false, giving a proof or a counterexample respectively?

Improve this question
$\endgroup$
0

1 Answer 1

Reset to default
2
$\begingroup$

Arguably we have had this since 1957, with the General Problem Solver. However, it is a thorny problem, and like so much in AI, it works fine in toy domains (like the Towers of Hanoi problem), but fails in real life, as real life is too complex for it to cope.

There is a list of solvers (the category of programs dealing with this issue) on Wikipedia. As of today, it comprises about 40 systems (split into two sub-categories). These work with mathematical equations and presumably also more general problems, assuming they are not too complex.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .