### Relaxed Weighted Path Order in Theorem Proving

Jan Jakubův, Cezary KaliszykMathematics in Computer Science, 14, pp. 657 – 670, 2020.

### Abstract

We propose an extension of the automated theorem prover E by the weighted path ordering (WPO). Weighted path ordering is theoretically stronger than all the orderings used in E however its parametrization is more involved than those normally used in automated reasoning. Inparticular, it depends on a term algebra. We integrate the ordering in E Prover and perform an evaluation on the standard theorem proving benchmarks. The ordering is complementary to the onesused in E prover so far.Furthermore, first-time presented here, we propose a relaxed variant of the weighted pathorder as an approximation of the standard WPO definition. A theorem prover strategy with a relaxedorder can be incomplete, which is, however, not an issue as completeness can be easily regainedby switching to a complete strategy. We show that the relaxed weighted path order can have a hugeimpact on an improvement of a theorem prover strategy.

### BibTeX

@article{jjck-mcs20, author = {Jan Jakubuv and Cezary Kaliszyk}, title = {Relaxed Weighted Path Order in Theorem Proving}, journal = {Math. Comput. Sci.}, volume = {14}, number = {3}, pages = {657--670}, year = {2020}, url = {https://doi.org/10.1007/s11786-020-00474-0}, doi = {10.1007/s11786-020-00474-0}, }