Abstract

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.

BibTeX

@inproceedings{jjck-icms18,
  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       = {https://doi.org/10.1007/978-3-319-96418-8\_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},
}