Solving Uninterpreted Equations with Context Free Expression Grammars
It is shown here that the equivalence class of an expression under the congruence closure of any finite set of equations between ground terms is a context free expression language. An expression is either a symbols or an n-tuple of expressions; the difference between expressions and strings is...
| Main Author: | |
|---|---|
| Language: | en_US |
| Published: |
2004
|
| Online Access: | http://hdl.handle.net/1721.1/6380 |