Prime Implicate Generation in Equational Logic

Mnacho Echenim, Nicolas Peltier, Sophie Tourret

JAIR 2017 pp. 827-880

doi:10.1613/JAIR.5481 /jair/2017/echenim2017jair-prime/

Abstract

A procedure is proposed to efficiently generate sets of ground implicates of first-order formulas with equality. It is based on a tuning of the superposition calculus, enriched with rules that add new hypotheses on demand during the proof search. Experimental results are presented, showing that the proposed approach is more efficient than state-of-the-art systems.

PDF JAIR Semantic Scholar

Cite

Text

Echenim et al. "Prime Implicate Generation in Equational Logic." Journal of Artificial Intelligence Research, 2017. doi:10.1613/JAIR.5481

Markdown

[Echenim et al. "Prime Implicate Generation in Equational Logic." Journal of Artificial Intelligence Research, 2017.](https://mlanthology.org/jair/2017/echenim2017jair-prime/) doi:10.1613/JAIR.5481

BibTeX

@article{echenim2017jair-prime,
  title     = {{Prime Implicate Generation in Equational Logic}},
  author    = {Echenim, Mnacho and Peltier, Nicolas and Tourret, Sophie},
  journal   = {Journal of Artificial Intelligence Research},
  year      = {2017},
  pages     = {827-880},
  doi       = {10.1613/JAIR.5481},
  volume    = {60},
  url       = {https://mlanthology.org/jair/2017/echenim2017jair-prime/}
}