[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #37

Originator: U. Reddy, F. Bronsard
Date:

Summary: Is there a notion of “complete theory” for which contextual deduction is complete for refutation of ground clauses?

In [BR91] a rewriting-like mechanism for clausal reasoning called “contextual deduction” was proposed. It specializes “ordered resolution” by using pattern matching in place of unification, only instantiating clauses to match existing clauses. Does contextual deduction always terminate? (In [BR91] it was taken to be obvious, but that is not clear; see also [NO90].) It was shown in [BR91] that the mechanism is complete for refuting ground clauses using a theory that contains all its “strong-ordered” resolvents. Is there a notion of “complete theory” (like containing all strong-ordered resolvents not provable by contextual refutation) for which contextual deduction is complete for refutation of ground clauses?

Contextual deduction as defined in [BR91] does not terminate. Bronsard and Reddy have gone on to solve this [BR93] by using a more restricted, decidable mechanism. A completeness proof, incorporating equational inference with complete systems, is given in [Bro95].

References

[BR91]
Francois Bronsard and Uday S. Reddy. Conditional rewriting in Focus. In M. Okada, editor, Proceedings of the Second International Workshop on Conditional and Typed Rewriting Systems, volume 516 of Lecture Notes in Computer Science, Montreal, Canada, 1991. Springer-Verlag.
[BR93]
F. Bronsard and U. S. Reddy. Reduction techniques for first-order reasoning. In M. Michaël Rusinowitch and J. L. Rémy, editors, Proceedings of the Third International Workshop on Conditional Rewriting Systems, volume 656 of Lecture Notes in Computer Science, pages 242–256, Pont-à-Mousson, France, January 1993. Springer-Verlag.
[Bro95]
Francois Bronsard. Using Term Orders to Control Deductions. PhD thesis, University of Illinois, 1995. Forthcoming.
[NO90]
Robert Nieuwenhuis and Fernando Orejas. Clausal rewriting. In S. Kaplan and M. Okada, editors, Extended Abstracts of the Second International Workshop on Conditional and Typed Rewriting Systems, pages 81–88, Montreal, Canada, June 1990. Concordia University. Revised version to appear in Lecture Notes in Computer Science, Springer-Verlag, Berlin.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]