Content deleted Content added
→Communities: +ja |
Added wiki-link to "Interactive theorem proving" |
||
Line 2:
The most developed subareas of automated reasoning probably
are [[automated theorem proving]] (and the less automated but more pragmatic subfield of [[interactive theorem proving]]) and [[automated proof checking]] (viewed as guaranteed correct reasoning under fixed assumptions), but extensive work has also been done in reasoning by [[analogy]], [[Induction (philosophy)|induction]] and [[Abductive reasoning|abduction]]. Other important topics are reasoning under [[uncertainty]] and [[Non-monotonic logic|non-monotonic]] reasoning. An important part of the uncertainty field is that of argumentation, where further constraints of minimality and consistency are applied on top of the more standard automated deduction. John Pollock's Oscar system is an example of an automated argumentation system that is more specific than being just an automated theorem prover. Formal argumentation is subfield of artificial intelligence.
Tools and techniques include the classical logics and calculi from automated theorem proving, but also [[fuzzy logic]], [[Bayesian inference]], reasoning with [[maximum entropy|maximal entropy]] and a large number of less formal ad-hoc techniques.
| |||