At its very beginning, the research field of automated reasoning (or, sometimes called computational

logic) has as part of its central global motivations the construction of software being able to generate (and

implicitly to solve) concrete mathematical works like for...