- Representation
- Reasoning
- Decidable
- Very powerful systems based on CDCL and DPLL

- Reliability
- Representation - 10%
- Reasoning - 90%

- Representation
- Individuals, classes, roles
- No way to denote non-explicit objects
- Mostly fragments of FOF

- Reasoning
- Designed to be decidable and tractable
- Some standard reasoning tasks, e.g., subsumption
- Some good, some buggy, ATP systems

- Reliability
- Representation - 35%
- Reasoning - 50%

- Representation
- Reasoning
- Decidable
- Some specialized approaches
- Some strong ATP systems

- Reliability
- Representation - 20%
- Reasoning - 80%

- Representation
- Reasoning
- Semi-decidable
- Well understood reasoning
- Mature, high-performance ATP systems

- Reliability
- Representation - 30%
- Reasoning - 70%

- Representation
- Full representation of objects
- Expressive set of "natural" connectives
- Variable quantifiers
- Example:
`PUZ130+1`

- Reasoning
- Semi-decidable
- Various techniques, mainly superposition on CNF
- Mature, fast ATP systems

- Reliability
- Representation - 50%
- Reasoning - 60%

- Representation
- Reasoning
- Semi-decidable
- Translation, early attempts
- Emerging modern techniques and implementations

- Reliability
- Representation - 60%
- Reasoning - 50%

- Representation
- Typed objects, connectives and quantifiers
- Numbers and arithmetic that reality needs
- Example:
`DAT002=1`

- Reasoning
- Undecidable due to arithmetic
- Spurred on by SMT
- Rapidly maturing ATP systems, but a tough nut

- Reliability
- Representation - 70%
- Reasoning - 25%

- Representation (without arithmetic)
- Typed objects, connectives and quantifiers
- Type constructors, polymorphic symbols
- Getting past non-technical users
- Example:
`PUZ139_2`

- Reasoning
- Monomorphization (sucks)
- A few implementations, not powerful (yet)

- Reliability
- Representation - 65%
- Reasoning - 40%

- Representation
- Typed objects, connectives and quantifiers
- Type constructors, polymorphic symbols
- FOOLish logic
- Example:
`FOO001_1`

- Reasoning
- Vampire, and only the Vampire

- Reliability
- Representation - 75%
- Reasoning - 20%

- Representation (without arithmetic)
- Reasoning
- Very mature ITP
- Maturing (and buggy) ATP

- Reliability
- Representation - 65%
- Reasoning - 40%

- Representation (without arithmetic)
- Lambda calculus and friends
- Type constructors, polymorphic symbols
- Great for mathematics and savvy mathematicians (not people)
- Example:
`PUZ000^1`

- Reasoning
- No ATP (yet)
- But coming soon, based on stable TH0

- Reliability
- Representation - 70%
- Reasoning - 30%

- Representation
- More than a human brain can handle
- Different flavours, and aquired taste

- Reasoning
- No ATP (in sight)

- Reliability
- Representation - 70%
- Reasoning - 10%