Equational theorem proving
2 methods in the atlas attack this one problem. They are rivals: each wins something the others do not.
Phrasings that mean this problem
Equational theorem proving
automated-reasoning
- Superposition calculusTerm-order restricted paramodulationstandardautomated-reasoning
- ParamodulationEquality replacement inferencespecialistautomated-reasoning