Relaxed Weighted Path Order in Theorem Proving

Jan Jakubův, Cezary Kaliszyk

Mathematics in Computer Science, 14, pp. 657 – 670, 2020.


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.


  PDF |    doi:10.1007/s11786-020-00474-0


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 = {},
doi = {10.1007/s11786-020-00474-0},
Nach oben scrollen