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},
}