Prime Implicate Generation in Equational Logic (extended abstract)
Prime Implicate Generation in Equational Logic (extended abstract)
Mnacho Echenim, Nicolas Peltier, Sophie Tourret
Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence
Journal track. Pages 5588-5592.
https://doi.org/10.24963/ijcai.2018/790
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.
Keywords:
Knowledge Representation and Reasoning: Automated Reasoning and Theorem Proving
Knowledge Representation and Reasoning: Diagnosis and Abductive Reasoning