Entailment Calculus as the Logical Basis of Automated Theorem Finding in Scientific Discovery
Jingde Cheng · 2002
) Jingde Cheng Department of Computer Science and Communication Engineering Kyushu University 6-10-1 Hakozaki, Fukuoka 812-81, Japan [email protected] woevC"oe"B | VqC"oCl\\"C 600 B.C. To attain knowledge, add things every day. To attain wisdom, remove things every day. |Lao Tzu, Tao Te Ching, ch.48, about 600 B.C. Abstract Any scientific discovery must include an epistemic process to gain knowledge of or to ascertain the existence of some empirical and/or logical entailments previously unknown or unrecognized. The epistemic operation of deduction in an epistemic process of an agent is to find new and valid entailments logically from some premises which are known facts and/or assumed hypothesis. Automated theorem finding can be regarded as the automation of deduction operations of an agent. This paper discusses the logical basis of automated theorem finding from the viewpoint of relevant logic. The paper points out why classical mathematical logic and/or...