Exercise 12
Herbrand Universe with Equality
Interpretation Quotient under Congruence
Herbrand Universe for Equality
Two major first-order provers:
Benchmarks and competition:
Some results achieved in Argone Labs
Reasoning about equations: Term Rewriting and All That, by Franz Baader and Tobias Nipkow