CS157 Fourth Unit Assignment: Category 5 -- Group Theory

The problems in this category are drawn from Group Theory. You are given the axioms shown below, and you may assume whatever equality axioms you deem appropriate. We will provide no additional premises. The conclusion in each case is a conjecture about Group Theory (which may, in some cases, be false).

The maximum number of steps for problems in this category is 10000 and the maximum depth is 20.

Your solution will contain the following:

  1. A rewriting of the Background Axioms
  2. An inference method: Logica or Epilog
  3. Strategies appropriate for your chosen inference method.

Background Axioms 

   (= (* (* ?x ?y) ?z) (* ?x (* ?y ?z)))
   (= (* ?x e) ?x)
   (= (* ?x (inv ?x)) e)

Sample Premises 

There will be no sample premises

Sample Conclusion 

   (= (* (inv a) a) e)