Validation And Verification Of Production Rules Using Rewrite Semantics

James G. Schmolze
Department of Electrical Engineering
and Computer Science
Tufts University

Friday, November 22, 1996
11 a.m. - 12 noon
Fuller Labs 320

I will begin by presenting a semantics for production rules based on term rewriting. The benefits of this semantic account are several. First, the account provides a standard by which to judge the correctness of any given production rule interpreter. Second, the account defines production rule execution over both ground memories and memory schemas; thus symbolic execution of production rules is well defined. Third, the account provides the basis for general solutions to several problems concerning validation and verification of production rule systems. I will briefly present the general solutions to three such problems.

  1. How can we detect redundant production rules?
  2. How can we test whether a production rule set is "confluent" (i.e., does it produce the same answer under any conflict resolution strategy?)?
  3. If a production rule set is not confluent, how can the computer assist in "completing" the rule set (i.e., change the rule set so that it is confluent)?

This work is based on term rewriting and Knuth-Bendix completion, and is joint work with Wayne Snyder of Boston University.

Maintained by webmaster@wpi.edu
Last modified: Sep 27, 2006, 16:05 EDT
[WPI] [Home] [Back] [Top]

Department of Computer Science - Worcester Polytechnic Institute
100 Institute Road, Worcester, MA 01609-2280
Phone: +1-508-831-5357 - Fax: +1-508-831-5776 - cs@wpi.edu