[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #85 (Solved !)

Originator: Michaël Rusinowitch
Date: April 1995

Summary: Can the restrictions on orderings for the use in ordered theorem proving strategies be relaxed?

Ordered paramodulation is known to be complete for simplification orderings that are total on ground terms [HR86]. Other theorem proving strategies are similarly restricted. How can these restrictions be relaxed?

Remark

[BGNR99] shows that it is sufficient for the ordering to be well-founded and to have the subterm property.

References

[BGNR99]

Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, and Albert Rubio. Paramodulation with non-monotonic orderings. In Fourteenth IEEE Annual Symposium on Logic in Computer Science, Trento, Italy, July 1999. IEEE.

[HR86]

Jieh Hsiang and Michaël Rusinowitch. A new method for establishing refutational completeness in theorem proving. In Jrg Siekmann, editor, 8th International Conference on Automated Deduction, volume 230 of Lecture Notes in Computer Science, pages 141–152, Oxford, England, 1986. Springer-Verlag.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]