Skip to Main content Skip to Navigation
Conference papers

Prime Implicate Generation in Equational Logic

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 [Nieuwenhuis and Rubio, 2001], 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.
Complete list of metadatas

Cited literature [2 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-01946497
Contributor : Nicolas Peltier <>
Submitted on : Thursday, November 7, 2019 - 1:46:57 PM
Last modification on : Thursday, July 9, 2020 - 9:44:46 AM
Document(s) archivé(s) le : Sunday, February 9, 2020 - 1:02:48 AM

File

EPT_IJCAI18.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01946497, version 1

Collections

Citation

Mnacho Echenim, Nicolas Peltier, Sophie Tourret. Prime Implicate Generation in Equational Logic. Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, 2018, Stockholm, Sweden. ⟨hal-01946497⟩

Share

Metrics

Record views

108

Files downloads

116