The Deep Encoding Answer

Problem

• SUO-KIF format problem file
  • 39 axioms
• TPTP format problem file
  • 45 axioms

Solution

• TPTP format proof (by SNARK)
  • 5 inferences
  • 12 axioms used
• In English:
  • As exchange rate is an instance of a ternary relation, and
    ternary relations are a subclass of relations, and
    class membership is transferred to superclasses,
    exchange rate is a relation.
  • As surface area and surface-to-volume ratio are binary relations, and
    binary relations are a subclass of relations, and
    class membership is transferred to superclasses,
    surface area and surface-to-volume ratio are relations.
  • As surface area is proportional to surface-to-volume ratio, and
    surface-to-volume ratio is proportional to exchange rate, and
    surface area, surface-to-volume ratio, and exchange rate are relations, and
    proportional relations are transitive,
    surface area is proportional to exchange rate.
  • As surface area is proportional to exchange rate, and
    surface area and exchange rate are relations, and
    proportional relations are symmetric,
    exchange rate is proportional to surface area.
  • As exchange rate is proportional to surface area,
    exchange rate is important, and
    exchange rate and surface area are relations, and
    importance is transferred by proportional relations,
    surface area is important.