home *** CD-ROM | disk | FTP | other *** search
/ Celestin Apprentice 4 / Apprentice-Release4.iso / Languages / Caml Light 0.7 / examples / kb / go.ml < prev    next >
Encoding:
Text File  |  1995-06-16  |  1.8 KB  |  72 lines  |  [TEXT/MPS ]
  1. #open "terms";;
  2. #open "order";;
  3. #open "kb";;
  4.  
  5. (* The axioms for groups *)
  6.  
  7. let group_rules = [
  8.   1, (1, (Term("*", [Term("U",[]); Var 1]), Var 1));
  9.   2, (1, (Term("*", [Term("I",[Var 1]); Var 1]), Term("U",[])));
  10.   3, (3, (Term("*", [Term("*", [Var 1; Var 2]); Var 3]),
  11.           Term("*", [Var 1; Term("*", [Var 2; Var 3])])))
  12. ];;
  13.  
  14. let group_precedence op1 op2 =
  15.   if op1 = op2 then Equal else
  16.   if (op1 = "I") or (op2 = "U") then Greater else NotGE
  17. ;;
  18.  
  19. let group_order = rpo group_precedence lex_ext 
  20. ;;
  21.  
  22. (* Another example *)
  23.  
  24. let geom_rules = [
  25.  1,(1,(Term ("*",[(Term ("U",[])); (Var 1)]),(Var 1)));
  26.  2,(1,(Term ("*",[(Term ("I",[(Var 1)])); (Var 1)]),(Term ("U",[]))));
  27.  3,(3,(Term ("*",[(Term ("*",[(Var 1); (Var 2)])); (Var 3)]),
  28.   (Term ("*",[(Var 1); (Term ("*",[(Var 2); (Var 3)]))]))));
  29.  4,(0,(Term ("*",[(Term ("A",[])); (Term ("B",[]))]),
  30.   (Term ("*",[(Term ("B",[])); (Term ("A",[]))]))));
  31.  5,(0,(Term ("*",[(Term ("C",[])); (Term ("C",[]))]),(Term ("U",[]))));
  32.  6,(0,
  33.   (Term
  34.    ("*",
  35.     [(Term ("C",[]));
  36.      (Term ("*",[(Term ("A",[])); (Term ("I",[(Term ("C",[]))]))]))]),
  37.   (Term ("I",[(Term ("A",[]))]))));
  38.  7,(0,
  39.   (Term
  40.    ("*",
  41.     [(Term ("C",[]));
  42.      (Term ("*",[(Term ("B",[])); (Term ("I",[(Term ("C",[]))]))]))]),
  43.   (Term ("B",[]))))
  44. ];;
  45.  
  46. let geom_rank = function
  47.     "U" -> 0
  48.   | "*" -> 1
  49.   | "I" -> 2
  50.   | "B" -> 3
  51.   | "C" -> 4
  52.   | "A" -> 5
  53.   |  _  -> failwith "Geom_rank"
  54. ;;
  55.  
  56. let geom_precedence op1 op2 =
  57.   let r1 = geom_rank op1
  58.   and r2 = geom_rank op2 in
  59.     if r1 = r2 then Equal else
  60.     if r1 > r2 then Greater else NotGE
  61. ;;
  62.  
  63. let geom_order = rpo geom_precedence lex_ext 
  64. ;;
  65.  
  66. kb_complete (gt_ord group_order) [] group_rules;;
  67.  
  68. (* If you have a fast machine, you may uncomment the following line: *)
  69.  
  70. (* print_newline(); kb_complete (gt_ord geom_order) [] geom_rules;; *)
  71.  
  72.