This goal is a bit complex in that it involves a little logic as well as a new lisp for me, zetalisp. Running lisp has fallen into this simple approach for me in the strange and wonderful MIT-CADR: I'm just re-LOADing a file to eval some changing imperative code. DEFVARs will not change an existing variable, but DEFPARAMETER will. I didn't think of a glib way to use this to keep some values while changing others, but it seems possible when LOADing a file repeatedly. Kinda kloodgey, but onto my planner plan. My current feeling about situation calculus is that there are fluents, which are predicates some of which are called executability preconditions, but I don't think that matters (to me at least). There are also actions. What I want from a planner is for it to put together a sequence of actions leading to some predicate/s becoming true. Now I want the plan to be informal and just be about sets of keywords with no necessarily deep meaning: However I want these informal keywords to be attached to lambda forms that are eventually intended to meet admissability under ACL2 first order logic's APPLY model. But for now I'm leaving the lambda forms empty and am concentrating on waving my arms informally. My figuring is that I have a list of entries like this: '(mnemonic-name consumes excludes yields witnesses lambdas) for example: '((pick-up-lock () (:lock) (:lock) () ()) (pick-up-key () (:key) (:key) () ()) (unlock (:lock :key) () (:treasure) () ())) and then what I am calling informal planning composes these actions, where complete plans require no CONSUMES but have a YIELDS containing the goal condition (:treasure in my eg). Both pick-ups consume nothing and produce (:lock :key) so a composite unlock plan of picking up the lock and key and then unlocking consumes nothing and results in :treasure. Broader goals are to highlight what I informally think I have done, and expose that to my first order automatic prover. I guess lambdas will be a lambda atom for fundamental actions, or a list of action entries for newly planned composite actions. I got a bit confused by how the default directory changes to match the last load?ed file, though it's pretty convenient. I resolved my FVWM screen hopping problem, where the lispm would then correct fvwm to where the mouse "really" was by using FVWM's mouse movement keyboard command to push the mouse between two screens as a way of straddling screens for the lispm.