| Examples are an important tool in Artificial Intelligence, especially in automated reasoning and machine learning. Early work has show that examples can be effectively used in automatic theorem proving. This thesis describes research on automatic example generation and applications of examples in a formal domain, namely, the Boyer-Moore theory.;A system called EGS has been implemented which automatically generates examples for a constraint stated in the theory. Examples are generated by successively refining a given constraint guided by certain kinds of knowledge. This knowledge includes function definitions, known examples, and equation solving procedures. EGS also rewrites constraint formulas and lemmas into simpler forms. EGS combines the methods of testing known examples and expanding definitions to achieve both efficiency and generality. Experiments have been performed using the EGS system to control backward chaining, one of the critical problem areas in the Boyer-Moore theorem prover. It has been found that irrelevant literals in conjectures, which are often introduced by the induction strategy of the theorem prover, prohibit effective use of examples in pruning unpromising backward chainings. Other potential applications of examples are also discussed. |
