Return to search

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

Identiferoai:union.ndltd.org:MIT/oai:dspace.mit.edu:1721.1/5683
Date01 April 1982
CreatorsMcAllester, David Allen
Source SetsM.I.T. Theses and Dissertation
Languageen_US
Detected LanguageEnglish
Format56 p., 16600403 bytes, 12407621 bytes, application/postscript, application/pdf
RelationAIM-667

Page generated in 0.0022 seconds