No TPTP formula. May not be expressible in strict first order.

Mid-level-ontology.kif 21688-21703

If a positive integer is a proton number of a pure substance, then if there exists an object such that the object is a part of the pure substance and the object is an instance of atom or the object is an instance of molecule, then there exists a symbolic string such that the positive integer is equal to the number of instances in the class described by the symbolic string

Sigma web home      Suggested Upper Merged Ontology (SUMO) web home
Sigma version 3.0 is open source software produced by Articulate Software and its partners