*SubtractionFn* | *documentation* If ?NUMBER1 *and* ?NUMBER2 are Numbers, then (*SubtractionFn* ?NUMBER1 ?NUMBER2) is the arithmetical difference *between* ?NUMBER1 *and* ?NUMBER2, i.e. ?NUMBER1 minus ?NUMBER2. An exception occurs when ?NUMBER1 is *equal* to 0, in which case (*SubtractionFn* ?NUMBER1 ?NUMBER2) is the negation of ?NUMBER2 | |

**has axiom** (*<=>* (*equal* (*AbsoluteValueFn* ?NUMBER1) ?NUMBER2) (or (*and* (*instance* ?NUMBER1 PositiveInteger) (*equal* ?NUMBER1 ?NUMBER2)) (*and* (*instance* ?NUMBER1 NegativeInteger) (*equal* ?NUMBER2 (*SubtractionFn* 0 ?NUMBER1)))))
| |

**has axiom** (=> (*equal* (*RoundFn* ?NUMBER1) ?NUMBER2) (or (=> (*lessThan* (*SubtractionFn* ?NUMBER1 (*FloorFn* ?NUMBER1)) .5) (*equal* ?NUMBER2 (*FloorFn* ?NUMBER1))) (=> (*greaterThanOrEqualTo* (*SubtractionFn* ?NUMBER1 (*FloorFn* ?NUMBER1)) .5) (*equal* ?NUMBER2 (*CeilingFn* ?NUMBER1)))))
| |

**has axiom** (*equal* (*MeasureFn* ?NUMBER *Celsius*) (*MeasureFn* (*SubtractionFn* ?NUMBER 273.15) *Kelvin*))
| |

**has domain1** Quantity | |

**has domain2** Quantity | |

**has ***identityElement* 0 | |

**has ***range* Quantity | |

**is an ***instance* of AssociativeFunction | |

**is an ***instance* of RelationExtendedToQuantities | |

BinaryFunction | **is first ***domain* of *distributes* | |

**is first ***domain* of *identityElement* | |

**is second ***domain* of *distributes* | |

Relation | **is first ***domain* of *domain* | |

**is first ***domain* of *domainSubclass* | |

**is first ***domain* of *holds* | |

**is first ***domain* of *subrelation* | |

**is first ***domain* of *valence* | |

**is second ***domain* of *subrelation* | |

Class | **is third ***domain* of *domain* | |

**is third ***domain* of *domainSubclass* | |

Abstract | **is ***disjoint* from Physical | |