Number Theory
- 285 abstract problems, 309 CNF problems
- Four axiomatizations
- Two older ones [LS74]
- Two built on NBG set theory [BL+86][Qua92]
- Those based on the NBG have the same properties ...
- Very general problems, some equality, CNF ones are non-Horn
- Hard challenges
Analysis
- 5 abstract problems, 19 CNF problems
- Second smallest mathematics domain in the TPTP
- Two axiomatization, all developed at ANL
- One old one [MOW76]
- One by Bledsoe [BL90]
- Mixture of problems
- With and without equality
- Horn and non-Horn
- Includes the Intermediate Value Theorem, e.g.,
ANA002-1.p
and "the sum of two continuous functions is continuous", e.g.,
ANA005-3.p