[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
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?
[BGNR99] shows that it is sufficient for the ordering to be well-founded and to have the subterm property.
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |