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...

Full description

Bibliographic Details
Main Authors: Feldman, Yishai A., Rich, Charles
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