HR

Theory Formation

• E.g., number theory, graph theory, group theory
• Given initial concepts about a domain
  • A concept has a definition and examples
• Production rules form new concepts from existing ones
• Empirical conjectures about concepts
  • No examples - non-existence conjecture
  • Same examples - equivalence conjecture
• Interface to ATP systems try to to settle conjectures
  • Axioms are provided
  • Theorem prover, e.g., Otter, to prove theorems
  • Model generator, e.g., MACE, to find counter examples

Example in Group Theory

• Given concepts of identity element and multiplication
• Forms the concepts of idempotent elements
• Conjectures: a*a=a ´ a = identity
• Otter proves this