Polymorphic Refinement

• KIF-Numbers included in Vectors

• + extended in Vectors with axiom:

  (=> (and (Vector ?x) (Vector ?y))
  
  (= (+ ?x ?y) (VectorAdd ?x ?y)))

• KIF-Numbers included in Strings

• + extended in Strings with axiom:

  (=> (and (String ?x) (String ?y))
  
  (= (+ ?x ?y) (Concat ?x ?y)))

• Strings and Vectors included in Extended-Arithmetic
  • Axioms from K-N, V, and S added to E-A
  • Public symbols from K-N, V, and S recognizable in E-A

• In E-A, + applies to numbers, vectors, and strings

Previous slide

Next slide

Back to first slide

View graphic version