Abstract

Tableaux-based provers work well for certain classes of first-order formulas and are better suited for integration with machine learning techniques. However, the tableaux techniques developed so far perform way worse than saturation-based techniques on the first-order formulas with equality. In this paper, we present the first implementation of Lazy Paramodulation which allows applying the ordering constraints in connection tableaux proof search without exponential blowup of the number of clauses (characteristic for Brand’s modifications). We implement the original Lazy Paramodulation calculus and propose a variant of the Brand’s modification (called LP-modification), which is based on the same ideas as Lazy Paramodulation, avoids exponential blowup and is just a preprocessing step for the standard Connection Tableaux calculus. We demonstrate the impact of both the Lazy Paramodulation and LP-modification on the proof search on a benchmark of TPTP library problems.

BibTeX

@inproceedings{gpck-paar22,
 author = {Grzegorz Prusak and Cezary Kaliszyk},
 booktitle = {Proceedings of the Workshop on Practical Aspects of Automated Reasoning, PAAR 2022},
 editor = {Boris Konev and Claudia Schon and Alexander Steen},
 publisher = {CEUR-WS.org},
 series = {{CEUR} Workshop Proceedings},
 title = {Lazy Paramodulation in Practice},
 url = {http://ceur-ws.org/Vol-3201/paper3.pdf},
 volume = {3201},
 year = {2022}
}