Pattern-Directed Invocation with Changing Equations
The interaction of pattern-directed invocation with equality in an automated reasoning system gives rise to a completeness problem. In such systems, a demon needs to be invoked not only when its pattern exactly matches a term in the reasoning data base, but also when it is possible to create a...
| Main Authors: | , |
|---|---|
| Language: | en_US |
| Published: |
2004
|
| Online Access: | http://hdl.handle.net/1721.1/6484 |
| _version_ | 1826210044035727360 |
|---|---|
| author | Feldman, Yishai A. Rich, Charles |
| author_facet | Feldman, Yishai A. Rich, Charles |
| author_sort | Feldman, Yishai A. |
| collection | MIT |
| description | The interaction of pattern-directed invocation with equality in an automated reasoning system gives rise to a completeness problem. In such systems, a demon needs to be invoked not only when its pattern exactly matches a term in the reasoning data base, but also when it is possible to create a variant that matches. An incremental algorithm has been developed which solves this problem without generating all possible variants of terms in the database. The algorithm is shown to be complete for a class of demons, called transparent demons, in which there is a well-behaved logical relationship between the pattern and the body of the demon. |
| first_indexed | 2024-09-23T14:40:37Z |
| id | mit-1721.1/6484 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T14:40:37Z |
| publishDate | 2004 |
| record_format | dspace |
| spelling | mit-1721.1/64842019-04-12T08:31:15Z Pattern-Directed Invocation with Changing Equations Feldman, Yishai A. Rich, Charles The interaction of pattern-directed invocation with equality in an automated reasoning system gives rise to a completeness problem. In such systems, a demon needs to be invoked not only when its pattern exactly matches a term in the reasoning data base, but also when it is possible to create a variant that matches. An incremental algorithm has been developed which solves this problem without generating all possible variants of terms in the database. The algorithm is shown to be complete for a class of demons, called transparent demons, in which there is a well-behaved logical relationship between the pattern and the body of the demon. 2004-10-04T14:57:52Z 2004-10-04T14:57:52Z 1988-05-01 AIM-1017 http://hdl.handle.net/1721.1/6484 en_US AIM-1017 4504217 bytes 1752074 bytes application/postscript application/pdf application/postscript application/pdf |
| spellingShingle | Feldman, Yishai A. Rich, Charles Pattern-Directed Invocation with Changing Equations |
| title | Pattern-Directed Invocation with Changing Equations |
| title_full | Pattern-Directed Invocation with Changing Equations |
| title_fullStr | Pattern-Directed Invocation with Changing Equations |
| title_full_unstemmed | Pattern-Directed Invocation with Changing Equations |
| title_short | Pattern-Directed Invocation with Changing Equations |
| title_sort | pattern directed invocation with changing equations |
| url | http://hdl.handle.net/1721.1/6484 |
| work_keys_str_mv | AT feldmanyishaia patterndirectedinvocationwithchangingequations AT richcharles patterndirectedinvocationwithchangingequations |