Reasoning Utility Package User's Manual, Version One
RUP (Reasoning Utility Package) is a collection of procedures for performing various computations relevant to automated reasoning. RUP contains a truth maintenance system (TMS) which can be used to perform simple propositional deduction (unit clause resolution) to record justifications, to tra...
| Main Author: | |
|---|---|
| Language: | en_US |
| Published: |
2004
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/5683 |
| _version_ | 1811089528030494720 |
|---|---|
| author | McAllester, David Allen |
| author_facet | McAllester, David Allen |
| author_sort | McAllester, David Allen |
| collection | MIT |
| description | RUP (Reasoning Utility Package) is a collection of procedures for performing various computations relevant to automated reasoning. RUP contains a truth maintenance system (TMS) which can be used to perform simple propositional deduction (unit clause resolution) to record justifications, to track down underlying assumptions and to perform incremental modifications when premises are changed. This TMS can be used with an automatic premise controller which automatically retracts "assumptions" before "solid facts" when contradictions arise and searches for the most solid proof of an assertion. RUP also contains a procedure for efficiently computing all the relevant consequences of any set of equalities between ground terms. A related utility computes "substitution simplifications" of terms under an arbitrary set of unquantified equalities and a user defined simplicity order. RUP also contains demon writing macros which allow one to write PLANNER like demons that trigger on various types of events in the data base. Finally there is a utility for reasoning about partial orders and arbitrary transitive relations. In writing all of these utilities an attempt has been made to provide a maximally flexible environment for automated reasoning. |
| first_indexed | 2024-09-23T14:20:20Z |
| id | mit-1721.1/5683 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T14:20:20Z |
| publishDate | 2004 |
| record_format | dspace |
| spelling | mit-1721.1/56832019-04-12T08:27:04Z Reasoning Utility Package User's Manual, Version One McAllester, David Allen reasoning utilities automated deduction backtracking stheorem proving truth maintenance dependencies demonic invocation RUP (Reasoning Utility Package) is a collection of procedures for performing various computations relevant to automated reasoning. RUP contains a truth maintenance system (TMS) which can be used to perform simple propositional deduction (unit clause resolution) to record justifications, to track down underlying assumptions and to perform incremental modifications when premises are changed. This TMS can be used with an automatic premise controller which automatically retracts "assumptions" before "solid facts" when contradictions arise and searches for the most solid proof of an assertion. RUP also contains a procedure for efficiently computing all the relevant consequences of any set of equalities between ground terms. A related utility computes "substitution simplifications" of terms under an arbitrary set of unquantified equalities and a user defined simplicity order. RUP also contains demon writing macros which allow one to write PLANNER like demons that trigger on various types of events in the data base. Finally there is a utility for reasoning about partial orders and arbitrary transitive relations. In writing all of these utilities an attempt has been made to provide a maximally flexible environment for automated reasoning. 2004-10-01T20:30:57Z 2004-10-01T20:30:57Z 1982-04-01 AIM-667 http://hdl.handle.net/1721.1/5683 en_US AIM-667 56 p. 16600403 bytes 12407621 bytes application/postscript application/pdf application/postscript application/pdf |
| spellingShingle | reasoning utilities automated deduction backtracking stheorem proving truth maintenance dependencies demonic invocation McAllester, David Allen Reasoning Utility Package User's Manual, Version One |
| title | Reasoning Utility Package User's Manual, Version One |
| title_full | Reasoning Utility Package User's Manual, Version One |
| title_fullStr | Reasoning Utility Package User's Manual, Version One |
| title_full_unstemmed | Reasoning Utility Package User's Manual, Version One |
| title_short | Reasoning Utility Package User's Manual, Version One |
| title_sort | reasoning utility package user s manual version one |
| topic | reasoning utilities automated deduction backtracking stheorem proving truth maintenance dependencies demonic invocation |
| url | http://hdl.handle.net/1721.1/5683 |
| work_keys_str_mv | AT mcallesterdavidallen reasoningutilitypackageusersmanualversionone |