Software engineering

• Add tests
• Implement a proper notion of printing environment
• Use proper logging
• Plug together the unification and the database again

Science

• Make sure the returned unifiers are minimal
• Add rigid variables

Indexation:

• Head
• Nb of arguments ("Equal" or "At least")
• Variances of constants
• Term indexing:
  To Read:
  • http://wwwlehre.dhbw-stuttgart.de/~sschulz/PAPERS/Schulz2013-FVI.pdf
  • Fingerprint Indexing for Paramodulation and Rewriting