Search Top Index
HELP RMS Bob Searle and Chris Mellish LIB RMS provides the basic facilities of a "Reason Maintenance System", as described in: "Truth Maintenance Systems for Problem Solving" Jon Doyle, MIT AI-TR-419, January 1978 (It has nothing to do with Record Management Services). This brief HELP file does not describe what a Reason Maintenance System is, but simply summarises the procedures provided by LIB RMS and LIB RMSAPPS. ---- LIB RMS --------------------------------------------------------------- The RMS deals with information in the form of NODES, which represent facts that are believed (IN) or disbelieved (OUT). The procedure for creating a new node is MAKENODE, which takes as its argument any structure which when printed out gives a readable rendering of what the fact is. For instance: makenode([nobody likes me])=> ** <node1> When printed out, for brevity a node comes out as the word "node" followed by a unique number. A fuller printout is obtained by use of the procedure SHOWNODE. If a node is to be believed, it must be JUSTIFIED. The procedure JUSTIFYNODE takes a node and two lists of nodes (the INLIST and the OUTLIST) and creates an SL justification for the node. The idea is that the node will be believed as long as it has a justification where everything in the INLIST is IN and everything in the OUTLIST is OUT. vars sun, nosun; makenode([the sun is shining]) -> sun; makenode([the sun is not shining]) -> nosun; justifynode(sun,[],[^nosun]); shownode(sun); <node1> [the sun is shining] IN <sl1> [] [<node2>] shownode(nosun); <node2> [the sun is not shining] OUT SHOWNODE gives the node number, human-readable form, and an indication as to whether the proposition is IN or OUT. If it is IN, it prints the "name" of one of its valid justification (here, "<sl1>"), together with the relevant INLIST and OUTLIST. The procedure RMSNODEISIN tests whether a node is IN or not. Eg. in the last example: rmsnodeisin(sun)=> ** <true> It may be useful to mark a node as CONTRADICTORY, using the procedure RMSCONTRADICT. Such a node should never come IN. Note that the system will only pay any attention to this information if it attempts to bring the node IN. If the node is already IN, nothing happens immediately. rmscontradict(nosun); shownode(nosun); <node2> [the sun is not shining] OUT ***contradiction*** If the system is ever about to bring IN a contradiction, it must sort things out so that, by suitably changing the status of assumptions made earlier, the contradiction is no longer believed. The procedure RMSFIXCONTRA is called automatically for this. The procedure takes as its argument the contradictory node. The default value of this procedure is RMSDEFFIXCONTRA, but the user may assign a new value to it. Defining such a procedure appropriately would require some study of the RMS code, however. ---- LIB RMSAPPS ----------------------------------------------------------- LIB RMSAPPS is not strictly necessary, but packages up some of the RMS facilities in some useful ways. The facilities provided are: NODES - a global variable, holding a list of all the RMS nodes created by the following procedures: DECLARE - takes one argument, calls MAKENODE on it, returns the node created and puts it on the list. The node is initially OUT. PREMISE - as DECLARE, except that the node is made IN by giving it a justification with INLIST and OUTLIST []. Returns the node as its result. ASSERT - takes three arguments. Calls DECLARE with the first and then justifies the resulting node with the other two. Returns the node as its result. SHOWINNODES - Three procedures for displaying the nodes in NODES. The SHOWOUTNODES first two call SHOWNODE on only IN and OUT nodes SHOWNODES respectively. The third calls SHOWNODE on all nodes. --- EXAMPLES OF USE OF THE RMS SYSTEM -------------------------------------- (1) MIDSUMMER PROBLEM ;;; this scenarion demostrates the use of dependancy-directed backtracking ;;; to resolve 'inconsistencies' in belief systems. ;;; thses inconsistencies are declared by the particular belief system and ;;; are enforced by rms. ;;; this example is based on Jon Doyle, (MIT AI-TR-419, January 1978) ;;; "Truth Maintenance Systems for Problem Solving" ;;; the story is that of Hermia, Lysander, Helena, and Demetrius from ;;; Wm. Shakespeare's "A Midsummer Night's Dream" ;;; get rms primed up to go lib rms; lib rmsapps; ;;; initialise list of interesting nodes [] -> nodes; ;;; declare some variables vars node, tragedy, hermia, lyshermia, demhermia, lyshelena; ;;; first declare the loves of the women as unchangeable premise([loves hermia lysander]) -> hermia; erase(premise([loves helena demetrius])); ;;; now declare the loves of the men as assumptions ;;; demetrius starts out loving hermia, but if this turns out ;;; to be unfortunate, he will turn his attentions to helena declare([not loves demetrius hermia]) -> node; assert([loves demetrius hermia],[],[^node]) -> demhermia; erase(assert([loves demetrius helena],[^node],[])); ;;; similarly, lysander loves hermia, ;;; but will settle for helena if required declare([not loves lysander hermia]) -> node; assert([loves lysander hermia],[],[^node]) -> lyshermia; assert([loves lysander helena],[^node],[]) -> lyshelena; ;;; unfortunately, lysander is a jealous man, ;;; and wants hermia for himself premise([jealous lysander]) -> node; ;;; being violent, this leads him to want to kill demetrius, ;;; because of both of their loves, and lysander's jealousy assert([kills lysander demetrius],[^node ^demhermia ^lyshermia],[]) -> node; showinnodes(); ;;; display what is currently believed ;;; since this is supposed to be a comedy, and killing isn't funny, ;;; the attempted murder is declared to be a tragedy ;;; first - we declare that a tragedy exists declare([tragedy]) -> tragedy; ;;; second - tell rms not to allow this to come about rmscontradict(tragedy); ;;; and, third - connect the attempted murder to the tragedy justifynode(tragedy,[^node],[]); ;;; display rms' resloution of the conflict showinnodes(); showoutnodes(); ;;; unfortunately, hermia is taking this situation badly, and is ;;; about to commit suicide from unrequited love, because her ;;; chosen one, lysander now loves another assert([suicide hermia],[^hermia ^lyshelena],[]) -> node; ;;; suicides aren't any better in comedies than murders, so this ;;; must also be declared a tragedy, and resolved by rms declare([tragedy 2]) -> tragedy; rmscontradict(tragedy); justifynode(tragedy,[^node],[]); ;;; this brings the story to a successful conclusion, viz: showinnodes(); ;;; the items not currently believed are: showoutnodes(); (2) DETECTION OF CIRCULAR REASONING ;;; demonstration of circular reasoning, ;;; and the detection of such by rms lib rms; lib rmsapps; vars node1, node2, node3, assump; [] -> nodes; premise('x+y=4') -> node1; declare('assume 1') -> assump; assert('x=1',[],[^assump]) -> node2; assert('y=3',[^node1 ^node2],[]) -> node3; shownodes(); justifynode(assump,[],[]); shownodes(); declare('assume 2') -> assump; justifynode(node3,[],[^assump]); justifynode(node2,[^node1 ^node3],[]); shownodes(); justifynode(assump,[],[]); shownodes();