Automated reasoning and Game playing
Automated Reasoning
Automated reasoning is an branch of computer science dedicated to understand different aspects of reasoning. It helps produce software which allows computers to reason completely or nearly completely, automatically. The subareas of automated reasoning are automated theorem proving and automated proof checking.
John Pollock’s Oscar system is an example of an automated argumentation system that is more specific than being just an automated theorem prover. The tools and techniques are:
- classic logic and calculi
- fuzzy logic
- Bayesian inference
- reasoning with maximal entropy
Significant Contribution
- Principia mathematics – Formal Logic
– derive all or some of the mathematical expressions in terms of symbolic logic.
- Logic Theorist (LT) – was developed to “mimic human reasoning” in proving theorems.
Applications
- build automated theorem provers e.g. LT
- applied to solve a growing number of problems in formal logic, mathematics, and computer science, logic programming software and hardware verification, circuit design and many other automated reasoning.
Game Playing
The system should be able to play more than one game at a time successfully. For making games like chess, computers are programmed to play these games using a specially designed algorithm, which cannot be transferred to another context. For eg. a chess playing computer program cannot play checkers. A general game playing system, if well designed, would be able to help in other areas, such as in providing intelligence for search and rescue missions.
The games are defined by sets of rules represented in the game description language. In order to play the games, players interact with a game hosting server that monitors move for legality and keeps players informed of state changes.