Towards a Unified Ordering for Superposition-Based Automated Reasoning

Jan Jakubuv, Cezary Kaliszyk

6th International Conference on Mathematical Software, Lecture Notes in Computer Science 10931, pp. 245 – 254, 2018.


We propose an extension of the automated theorem prover E by the weighted path ordering. Weighted path ordering is theoretically stronger than all the orderings used in E-prover, however its parametrization is more involved than those normally used in automated reasoning. In particular, it depends on a term algebra. We discuss how the parameters for the ordering can be proposed automatically for particular theorem proving problem strategies. We integrate the ordering in E-prover and perform an evaluation on the standard theorem proving benchmarks. The ordering is complementary to the ones used in E prover so far.


   doi:10.1007/978-3-319-96418-8_29  |   © Standard Springer LNCS Copyright


author = {Jan Jakubuv and Cezary Kaliszyk},
title = {Towards a Unified Ordering for Superposition-Based Automated Reasoning},
booktitle = {6th International Conference on Mathematical Software (ICMS 2018)},
pages = {245--254},
year = {2018},
url = {\_29},
doi = {10.1007/978-3-319-96418-8\_29},
editor = {James H. Davenport and Manuel Kauers and George Labahn and Josef Urban},
series = {LNCS},
volume = {10931},
publisher = {Springer},
year = {2018},
Nach oben scrollen