|
Most work in logic rather than mathematics. Some work in program synthesis. Resolution theorem proving. Non resolution methods. Ammon's system uses heuristics. See also Alan Bundy |
Most work in automated reasoning has been in the field of logic rather than mathematics. Automated reasoning has also been applied in the automatic synthesis of programs from input output examples or formal specifications. The most common technique has been resolution theorem proving. Other methods have been favoured by Bledsoe. The most advanced system for doing real mathematics is Ammon's SHUNYATA system which uses a large number of hand crafted heuristics. A good survey of automated reasoning is Alan Bundy's book "Introduction to Mathematical Reasoning". |
|
|
|
|
|
|