Rewrite-based deduction and symbolic constraints

摘要

Bulding a state-of-the-art theorem prover requires the combination of at least three main ingredients: good theory, clever heuristics, and the necessary engineering skills to implement it all in an efficient way. Progress in each of these ingredients interacts in different ways.