1990 | ReviewPaper | Buchkapitel
On restrictions of ordered paramodulation with simplification
verfasst von : Leo Bachmair, Harald Ganzinger
Erschienen in: 10th International Conference on Automated Deduction
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We consider a restricted version of ordered paramodulation, called strict superposition. We show that strict superposition (together with equality resolution) is refutationally complete for Horn clauses, but not for general first-order clauses. Two moderate enrichments of the strict superposition calculus are, however, sufficient to establish refutation completeness. This strictly improves previous results. We also propose a simple semantic notion of redundancy for clauses which covers most simplification and elimination techniques used in practice yet preserves completeness of the proposed calculi. The paper introduces a new and comparatively simple technique for completeness proofs based on the use of canonical rewrite systems to represent equality interpretations.