Questions tagged [automated-reasoning]

For questions about Automated Reasoning concepts and research topics. Automated Reasoning is a sub-field of Artificial Intelligence concerned with the development of computer programs which can reason completely, or nearly completely, automatically.

Automated Reasoning (AR) is a sub-field of Artificial Intelligence concerned with the development of computer programs which can reason completely, or nearly completely, automatically.

Example of applications are automated theorem proving, proof checking, logic programming, circuit design and reasoning under uncertainity.

Tools used in AR include formal logic, fuzzy logic, bayesian inference and other formal ad-hoc techniques.

One of the first example of successful AR is Logic Theorist (LT), a computer program developed in 1956 by Allen Newell, Cliff Shaw and Herbert A. Simon, which eventually proven 38 of the first 52 theorems in Whitehead and Russell's Principia Mathematica, and find new and more elegant proofs for some. It is called "the first artificial intelligence program".

5 questions
16
votes
1 answer

Why is automated theorem proving so hard?

The problem of automated theorem proving (ATP) seems to be very similar to playing board games (e.g. chess, go, etc.): it can also be naturally stated as a problem of a decision tree traversal. However, there is a dramatic difference in progress on…
7
votes
1 answer

Did Turing foresee the required capabilities to pass the Turing test?

In Section 1.1 of Artificial Intelligence: A Modern Approach, it is stated that a computer which passes the Turing Test would need 4 capabilities, and that these 4 capabilities comprise most of the field of Artificial Intelligence: natural language…
4
votes
2 answers

Is there a machine learning system that is able to understand mathematical problems given in a textual description?

Is there a machine learning system that is able to "understand" mathematical problems given in a textual description, such as A big cat needs 4 days to catch all the mice and a small cat needs 12 days. How many days need both, if they catch mice…
1
vote
1 answer

When will we have computer programs that can compose mathematical proofs?

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?
1
vote
0 answers

What is the difference between Knowledge Representation and Automated Reasoning?

Knowledge Representation and Automated Reasoning are two AI subfields which seem to have something to do with reasoning. However, I can't find any information online about their relationship. Are they synonyms? Is KR a subfield of AR? What's the…