The Interaction Between Truth Maintenance, Equality, and Pattern-Directed Invocation: Issues of Completeness and Efficiency
We have implemented a reasoning system, called BREAD, which includes truth maintenance, equality, and pattern-directed invocation. This paper reports on the solution of two technical problems arising out of the interaction between these mechanisms. The first result is an algorithm which ensures the...
Main Authors: | , |
---|---|
Format: | Working Paper |
Language: | en_US |
Published: |
MIT Artificial Intelligence Laboratory
2008
|
Online Access: | http://hdl.handle.net/1721.1/41187 |
_version_ | 1826193215662850048 |
---|---|
author | Feldman, Yishai A. Rich, Charles |
author_facet | Feldman, Yishai A. Rich, Charles |
author_sort | Feldman, Yishai A. |
collection | MIT |
description | We have implemented a reasoning system, called BREAD, which includes truth maintenance, equality, and pattern-directed invocation. This paper reports on the solution of two technical problems arising out of the interaction between these mechanisms. The first result is an algorithm which ensures the completeness of pattern-directed invocation with respect to equality. The second result is an algorithm which reduces a class of redundant proofs. |
first_indexed | 2024-09-23T09:35:28Z |
format | Working Paper |
id | mit-1721.1/41187 |
institution | Massachusetts Institute of Technology |
language | en_US |
last_indexed | 2024-09-23T09:35:28Z |
publishDate | 2008 |
publisher | MIT Artificial Intelligence Laboratory |
record_format | dspace |
spelling | mit-1721.1/411872019-04-12T09:32:24Z The Interaction Between Truth Maintenance, Equality, and Pattern-Directed Invocation: Issues of Completeness and Efficiency Feldman, Yishai A. Rich, Charles We have implemented a reasoning system, called BREAD, which includes truth maintenance, equality, and pattern-directed invocation. This paper reports on the solution of two technical problems arising out of the interaction between these mechanisms. The first result is an algorithm which ensures the completeness of pattern-directed invocation with respect to equality. The second result is an algorithm which reduces a class of redundant proofs. MIT Artificial Intelligence Laboratory 2008-04-15T15:00:33Z 2008-04-15T15:00:33Z 1987-05 Working Paper http://hdl.handle.net/1721.1/41187 en_US MIT Artificial Intelligence Laboratory Working Papers, WP-296 application/pdf MIT Artificial Intelligence Laboratory |
spellingShingle | Feldman, Yishai A. Rich, Charles The Interaction Between Truth Maintenance, Equality, and Pattern-Directed Invocation: Issues of Completeness and Efficiency |
title | The Interaction Between Truth Maintenance, Equality, and Pattern-Directed Invocation: Issues of Completeness and Efficiency |
title_full | The Interaction Between Truth Maintenance, Equality, and Pattern-Directed Invocation: Issues of Completeness and Efficiency |
title_fullStr | The Interaction Between Truth Maintenance, Equality, and Pattern-Directed Invocation: Issues of Completeness and Efficiency |
title_full_unstemmed | The Interaction Between Truth Maintenance, Equality, and Pattern-Directed Invocation: Issues of Completeness and Efficiency |
title_short | The Interaction Between Truth Maintenance, Equality, and Pattern-Directed Invocation: Issues of Completeness and Efficiency |
title_sort | interaction between truth maintenance equality and pattern directed invocation issues of completeness and efficiency |
url | http://hdl.handle.net/1721.1/41187 |
work_keys_str_mv | AT feldmanyishaia theinteractionbetweentruthmaintenanceequalityandpatterndirectedinvocationissuesofcompletenessandefficiency AT richcharles theinteractionbetweentruthmaintenanceequalityandpatterndirectedinvocationissuesofcompletenessandefficiency AT feldmanyishaia interactionbetweentruthmaintenanceequalityandpatterndirectedinvocationissuesofcompletenessandefficiency AT richcharles interactionbetweentruthmaintenanceequalityandpatterndirectedinvocationissuesofcompletenessandefficiency |