Definitions and algorithms for First-Order Logic, working towards saturation-based inductive provers