Invited Talk: Rewrite-Based Deduction and Symbolic Constraints

Building 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.On the one hand, new theoretical insights replace heuristics by more precise and effective techniques. For example, the completeness proof of basic paramod- ulation [NR95,BGLS95] shows why no inferences below Skolem functions are needed, as conjectured by McCune in [McC90]. Regarding implementation tech- niques, ad-hoc algorithms for procedures like demodulation or subsumption are replaced by efficient, re-usable, general-purpose indexing data structures for which the time and space requirements are well-known.