%--------------------------------------- % Foundations of Language Interaction % Program Four: Intention Recognition and Collaboration % M. Stone, 6-14-01 and 6-21-01 % mdstone@cs.rutgers.edu %--------------------------------------- %--------------------------------------- % Basic definitions -- % - Definitions for debugging % - List Processing %--------------------------------------- module Basic. % printing messages can be conditioned % on either of these two propositions; % then query % (verbose => g) % or % (debug => g) % in place of g to get feedback about execution. type verbose o. type debug o. % (status S) % always succeeds, but if "verbose" is true, % it prints S to the terminal as a side-effect. type status string -> o. status S :- verbose, !, output std_out S. status S. % (message S) % always succeeds, but if "debug" is true, % it prints S to the terminal as a side-effect. type message string -> o. message S :- debug, !, output std_out S. message S. type vacuous_assumption o. % some list functions... type head list A -> list A -> o. type member A -> list A -> o. type pmember A -> list A -> B -> list B -> o. type remove_elt A -> list A -> list A -> o. type remove list A -> list A -> list A -> o. type sublist list A -> list A -> o. type disjoint list A -> list A -> o. type union list A -> list A -> list A -> o. head (A :: _) (A ::nil). head nil nil. % (member A L) if A is an element of L. member A (A :: R). member A (H :: R) :- member A R. % (pmember A L B M) if A is nth element of L and % b is nth element of M pmember A (A :: R) B (B :: S). pmember A (H :: R) B (I :: S) :- pmember A R B S. % (sublist L1 L2) if % every element of L1 is an element of L2. sublist nil L. sublist (E::R) L :- member E L, sublist R L. % (remove_elt A L1 L2) if % L2 is like L1 except that % all occurrences of A are % omitted in L2. remove_elt A nil nil. remove_elt A (A::R) G :- !, remove_elt A R G. remove_elt A (E::R) (E::L) :- remove_elt A R L. % (remove R L1 L2) if % L2 is like L1 except that % all occurrences of elements of R % are omitted in L2. remove nil L L. remove (A::R) L F :- remove_elt A L M, remove R M F. % (disjoint L R) if % L and R have no elements in common. disjoint L R :- not (sigma e\ (member e L, member e R)). % (union X Y Z) if % Z is a list with the elements of % X in order followed by the elements % of Y in order. union nil R R. union (A::L) R (A::U) :- union L R U. % filterpreda L R G E % if G contains the list of first elements that % are R related to the elements of L, followed % by the elements of E. type filterpreda list A -> (A -> B -> o) -> list B -> list B -> o. filterpreda nil F End End. filterpreda (A::As) F (B::Bs) End :- F A B, !, filterpreda As F Bs End. filterpreda (_::As) F Bs End :- filterpreda As F Bs End. type foreach (A -> o) -> list A -> o. foreach P nil. foreach P (H::T) :- P H, foreach P T. type pelts (A -> o) -> list A -> list A -> o. pelts P nil nil. pelts P (H::T) (H::R) :- P H, !, pelts P T R. pelts P (_::T) R :- pelts P T R. %%%%%%%%%%%%%%%%% %--------------------------------------- % Truth in knowledge databases. %--------------------------------------- module LK. import Basic. kind agent, object, fact type. %--------------------------------------- % Building blocks of a logic of knowledge. % k A F : agent A knows fact F % g A G : agent A wants goal G % sm x\FL x : there is an x for which % all the facts in (FL x) are true. %--------------------------------------- type k agent -> fact -> fact. type g agent -> fact -> fact. type sm (object -> list fact) -> fact. type self agent. type other agent. type all agent. type done fact. type incorrect fact -> fact. %--------------------------------------- % Match F G % true if G follows when F is true. % Builds in simple relationships among % modalities, so as to automate the % inferences of veridicality and % positive introspection (with search). % Cuts ensure one F-G match, avoiding % ambiguities with multiple operators. % No reasoning with existential quantifiers % (existential quantifiers are handled % in the structure of plan-proofs) %--------------------------------------- type m_match agent -> agent -> o. m_match all Any. m_match self self. m_match other other. type match fact -> fact -> o. % Axiom. match F F :- !. % Veridicality. match (k A F) G :- match F G, !. % Positive introspection. match (k A F) (k B G) :- m_match A B, match (k A F) G, !. % (partner A O) % is true if O is the person A's talking to. type partner agent -> agent -> o. partner self other. partner other self. % (describes A F) % is true if the fact F constitutes % exclusively a description of agent % A's mental state. type describes agent -> fact -> o. describes A (k B _) :- m_match B A, !. describes A (g B _) :- m_match B A, !. describes Agent (k _ F) :- describes Agent F. describes Agent (g _ F) :- describes Agent F. describes Agent (sm P) :- pi o\ foreach (describes Agent) (P o). % (strip_ks A F) % is true if F can be obtained from A % by stripping off initial k's. type strip_ks fact -> fact -> o. strip_ks A A. strip_ks (k Ag A) F :- strip_ks A F. %--------------------------------------- % Entailment % does one body of facts follow % from another; computed using match. % entail_one KB G % true if F follows from KB. % multiple matches are appropriate % since they may involve distinct % values for variables. % entail_all KB Gs % true if all Gs follow from KB. %--------------------------------------- type entail_one list fact -> fact -> o. entail_one (F::_) G :- match F G. entail_one (_::Fs) G :- entail_one Fs G. type entail_all list fact -> list fact -> o. entail_all KB nil. entail_all KB (G::Gs) :- entail_one KB G, entail_all KB Gs. %--------------------------------------- % know_all Ag KB Gs % like entail_all, but true only if % each fact in Gs is of the form % (k Ag G). %--------------------------------------- type know_all agent -> list fact -> list fact -> o. know_all Ag KB nil. know_all Ag KB ((k Ag G) :: Gs) :- entail_one KB (k Ag G), know_all Ag KB Gs. %--------------------------------------- % make_known A Fs KB % shortcut for perception: true if % KB is a list of (k A F) for each % F in Fs. %--------------------------------------- type make_known agent -> list fact -> list fact -> o. make_known Ag nil nil. make_known Ag (F :: Fs) ((k Ag F) :: Gs) :- make_known Ag Fs Gs. %--------------------------------------- % goal_desc A KB Gs % know_desc A KB Ks % narrows KB to restrict it to just % those facts that describe the goals (Gs) % or knowledge (Ks) of agent A. %--------------------------------------- type goal_desc agent -> list fact -> list fact -> o. goal_desc A nil nil. goal_desc A (F :: Fs) (G :: Gs) :- match F (g A G), !, goal_desc A Fs Gs. goal_desc A (F :: Fs) Gs :- goal_desc A Fs Gs. type know_desc agent -> list fact -> list fact -> o. know_desc A nil nil. know_desc A (F :: Fs) (F :: Gs) :- match F (k A G), !, know_desc A Fs Gs. know_desc A (F :: Fs) Gs :- know_desc A Fs Gs. %%%%%%%%%%%%%% %--------------------------------------- % Constraint Processing % This module supports two parameterized types, % - a type we associating an element with a weight. % - a type ui representing a context with any % number of placeholders. %--------------------------------------- module Findall. import Basic. %--------------------------------------- % we: Weighted Element % (w A N) weights object A by integer N %--------------------------------------- kind we type -> type. type w A -> int -> we A. %--------------------------------------- type weight_all int -> list A -> list (we A) -> o. % (weight_all N L L') % true if L' is the list of elements of L weighted by N. weight_all N nil nil. weight_all N (H::T) (w H N::R) :- weight_all N T R. %--------------------------------------- type unweight we A -> A -> o. % (unweight W A) % true if A is the element in W. unweight (w A _) A. %--------------------------------------- type best list (we A) -> list (we A) -> o. type bh list (we A) -> int -> list (we A) -> list (we A) -> o. % (best L B) % true if B is the list of elements of L with lowest weight. % (bh L-To-Go Best-Value-So-Far Best-Elements-So-Far Eventual-Result) % best helper bh nil B L L. bh (w H W::R) B Bs L :- W = B, bh R B (w H W::Bs) L. bh (w H W::R) B Bs L :- W < B, bh R W (w H W::nil) L. bh (w H W::R) B Bs L :- W > B, bh R B Bs L. best nil nil. best (w H W::R) L :- bh R W (w H W :: nil) L. %--------------------------------------- % ui A % is the type of UnInstantiated elements % of type A. % We can think of an uninstantiated element as % an expression of type A containing an % arbitrary number of holes. In the ui A type, % each hole is represented as a lambda-bound % variable. %--------------------------------------- kind ui type -> type. %--------------------------------------- % the type has two constructors. % (i A) for INSTANCE % gives the matrix expression with holes % (u F) for UNDETERMINED % uses the function F to lambda-bind one % hole away. type i A -> ui A. type u (B -> ui A) -> ui A. %--------------------------------------- type fits ui A -> A -> o. % (fits Context Instance) % is true if Instance can be obtained % by substituting appropriate values for % the holes in the Context. fits (i A) A. fits (u F) A :- fits (F X) A. %--------------------------------------- type lift1 (A -> o) -> (ui A -> o). % (lift1 Predicate Context) % is true if Predicate applies % to every instance of the Context. lift1 R (i A) :- R A. lift1 R (u F) :- pi o \ lift1 R (F o). %--------------------------------------- type lift2 (A -> B -> o) -> (ui A -> ui B -> o). % (lift2 Relation C1 C2) % is true if Relation relates every % instance of C1 whose holes are instantiated % to a sequence of values V to a corresponding % instance of C2 whose holes are instanted to V. lift2 R (i A) (i B) :- R A B. lift2 R (u F) (u G) :- pi o \ lift2 R (F o) (G o). %--------------------------------------- type lift3 (A -> B -> C -> o) -> (ui A -> ui B -> ui C -> o). % (lift3 Relation C1 C2 C3) % is true if Relation relates every instance of % C1 whose holes are instanted to a sequence of values % V to corresponding instances of C2 and C4 whose holes % are also instantiated to V. lift3 R (i A) (i B) (i C) :- R A B C. lift3 R (u F) (u G) (u H) :- pi o \ lift3 R (F o) (G o) (H o). % linguists will recognize the expression % lift3 (p\q\c\ c=(p,q)) % -- whose type is (ui o -> ui o -> ui o -> o) -- % as Partee and Rooth's generalized conjunction. %------------ % Lists with holes %--------------------------------------- type null ui (list A) -> o. % An unstantiated list is null if every instance is nil. null E :- lift1 (x\x = nil) E. %--------------------------------------- type cons ui (list A) -> ui A -> ui (list A) -> o. % (Cons Lf Hf Tf) % True if Lf is a list context every instance V % of which is a nonempty list. If so, Hf is % the context that, when instantiated to V, gives % the head of the list Lf V, and Tf is the context % that, when instantiated to V, gives the tail of % the list Lf V. cons E H T :- lift3 (l\h\t\ l = h::t) E H T. %----------------------------------------------- type all_pred_members (A -> B -> o) -> ui A -> list B -> list (ui A) -> o. % (all_pred_members Relation Pattern Relata Matches) % true if Matches are all the instances of Pattern % which are related to an element of the list Relata % by Relation. % Assumes that all the elements of Relata are ground, % and that for each B in Relata there is at most one % ground instance A related by (Relation A B). all_pred_members Pd Af nil nil. all_pred_members Pd Af (B::T) (VAf::R) :- fits Af A, Pd A B, !, lift2 (x\y\y = A) Af VAf, all_pred_members Pd Af T R. all_pred_members Pd Af (_::T) R :- all_pred_members Pd Af T R. %----------------------------------------------- % The types % ui A and we A % are helpers for a pair of constraint-satisfaction % solvers. % A constraint is implemented as an expression of % type ui A: it is some A with placeholders for % the variables that need to be solved for. % Instances are also expressions of type ui A: % when a constraint variable is instantiated, % the corresponding hole in the instance does not % occur in the ultimate expression; on the other hand, % when the constraint variable is not instantiated, % meaning that any value for the variable satisfies % the constraint, the instance retains a hole for % the variable that can be instantiated in different % ways. % All the constraints can therefore be regarded % as an expression of type ui(list A) and the set % of satisfying instances of the constraint-set is % also an expression of type ui(list A). % The basic operation in constraint solving is to % work recursively -- finding the matches for the first % constraint and the matches for the rest of the % constraints -- and whenever possible unifying the % matches into a single term that records the combined % match to the first constraint and the rest of % the constraints. %----------------------------------------------- %----------------------------------------------- type unify ui (list A) -> ui A -> ui (list A) -> ui (list A) -> o. type abstract_if_possible A -> A -> (A -> ui (list B)) -> ui (list B) -> o. % (unify Constraints FirstInstance RestInstance FullInstance) % is true if FullInstance represents a context % corresponding to Constraints which combines % the instance FirstInstance of the head of % Constraints with the instance RestInstance of % the rest of constraints. % The definition of unify is a bit convoluted % to instantiate hole-variables correctly when there are % different occurences of holes in the HeadPattern and % TailPattern. A free variable in one should take its % value from its instance in the other -- but when both % are free, we should represent a free variable in the % result. unify (i (H::T)) (i H) (i T) (i (H::T)). unify (u ConsF) (u Hf) (u Tf) (u Result) :- pi o \ sigma X \ sigma RExpr \ (unify (ConsF X) (Hf X) (Tf X) RExpr, abstract_if_possible X o Result RExpr). abstract_if_possible X X F (F X) :- !. abstract_if_possible X Y (x\R) R. %----------------------------------------------- type fill ui A -> list (ui (list A)) -> ui (list A) -> list (ui (list A)) -> list (ui (list A)) -> o. % (fill MatchForHead MatchesForTails Constraints % FillList Afterwards) % true if FillList contains first the list of instances % that represent a combination of MatchForHead % with an element of MatchesForTails and that % instantiate the constraints Constraints, and % thereafter continues with the list Afterwards. fill Hi nil _ Rest Rest. fill Hi (Ti::Tis) Expr (HTi::More) Rest :- unify Expr Hi Ti HTi, !, fill Hi Tis Expr More Rest. fill Hi (_::Tis) Expr More Rest :- fill Hi Tis Expr More Rest. %----------------------------------------------- type combine list (ui A) -> list (ui (list A)) -> ui (list A) -> list (ui (list A)) -> o. % (combine MatchesForHead MatchesForTails Constraints Matches) % true if Matches contains all the instances of Constraints % that can be obtained by unifying an element of MachesForHead % with an element of MatchesForTails. combine nil _ _ nil. combine (Hi :: His) Tis Expr All :- fill Hi Tis Expr All Others, combine His Tis Expr Others. %----------------------------------------------- type solutions (ui A -> list (ui A) -> o) -> ui (list A) -> list (ui (list A)) -> o. % (solutions InstancePredicate Pattern Solutions) % Assumes that InstancePredicate can be called on % any individual constraint of type ui A to give % a list of the instances that satisfy the individual % constraint. % True if Solutions is the list of instances of % Pattern where InstancePredicate will succeed on % each component of Pattern. solutions Instances Expr (Nil::nil) :- null Expr, lift2 (x\y\ y = nil) Expr Nil. solutions Instances Expr Solutions :- cons Expr Hf Tf, Instances Hf His, solutions Instances Tf Tis, combine His Tis Expr Solutions. %----------------------------------------------- type findall ui (list A) -> list A -> list (ui (list A)) -> o. % (findall Constraint DB Answers) % findall illustrates how the constraint solver % can be called. It assumes that the matches % are given ahead of time as a database of true % ground instances DB. Answers is returned as % the list of instances of Constraints that are % satisfied in DB. findall Constraint DB Answers :- solutions (i\a\ all_pred_members (x\y\x = y) i DB a) Constraint Answers. %----------------------------------------------- % We now consider weighted constraint satisfaction. % % Weighted constraint satisfaction is like % constraint satisfaction except that each % instance of any constraint is associated with % an integer representing the cost of the % solution. The cost of a list of instances % is the sum of the cost of the instances. % The predicates can be used to compute % "least cost" solutions to constraints. % % The organization of the code parallels solutions. %----------------------------------------------- %----------------------------------------------- type w_fill (we (ui A)) -> list (we (ui (list A))) -> ui (list A) -> list (we (ui (list A))) -> list (we (ui (list A))) -> o. % (w_fill MatchForHead MatchesForTails Constraints % FillList Afterwards) % true if FillList contains first the list of WEIGHTED % instances that represent a combination of MatchForHead % with an element of MatchesForTails and that % instantiate the constraints Constraints, and % thereafter continues with the list Afterwards. w_fill Whi nil _ Rest Rest. w_fill (w Hi Wh) ((w Ti Wt)::Wtis) Expr (w HTi Sum::More) Rest :- unify Expr Hi Ti HTi, !, Sum is Wh + Wt, w_fill (w Hi Wh) Wtis Expr More Rest. w_fill Whi (_::Wtis) Expr More Rest :- w_fill Whi Wtis Expr More Rest. %----------------------------------------------- type w_combine list (we (ui A)) -> list (we (ui (list A))) -> ui (list A) -> list (we (ui (list A))) -> o. % (w_combine MatchesForHead MatchesForTails Constraints Matches) % true if Matches contains all the WEIGHTED instances of % Constraints that can be obtained by unifying an element % of MachesForHead with an element of MatchesForTails, and % computing a corresponding total weight. w_combine nil _ _ nil. w_combine (Whi :: Whis) Wtis Expr All :- w_fill Whi Wtis Expr All Others, w_combine Whis Wtis Expr Others. %----------------------------------------------- type w_solutions (ui A -> list (we (ui A)) -> o) -> ui (list A) -> list (we (ui (list A))) -> o. % (w_solutions InstancePredicate Pattern Solutions) % Assumes that InstancePredicate can be called on % any individual constraint of type ui A to give % a list of the WEIGHTED instances that satisfy the % individual constraint. % True if Solutions is the list of WEIGHTED instances of % Pattern where InstancePredicate will succeed on % each component of Pattern. %----------------------------------------------- type warn ui (list A) -> list (we (ui A)) -> list (we (ui (list A))) -> o. % (warn Constraint Instances Result) % for the moment, if debug is on, prints a record % of the constraint satisfaction process so far. warn Expr Insts nil :- debug, !, term_to_string Expr X, output std_out "Plan recognition fails for conflicting constraints \n", output std_out X, output std_out "\n", output std_out "instances are:\n", foreach (i\ sigma u\ sigma f\ sigma n\sigma s\ (i = (w u n), term_to_string u s, output std_out s, output std_out "\n")) Insts. warn Expr Insts All :- debug, !, output std_out "instances are:\n", foreach (i\ sigma u\ sigma f\ sigma n\sigma s\ (i = (w u n), term_to_string u s, output std_out s, output std_out "\n")) Insts, output std_out "solutions are:\n", foreach (i\ sigma u\ sigma f\ sigma n\sigma s\ (i = (w u n), term_to_string u s, output std_out s, output std_out "\n")) All. warn _ _ _. %----------------------------------------------- w_solutions Instances Expr (w Nil 0::nil) :- null Expr, lift2 (x\y\y = nil) Expr Nil. w_solutions Instances Expr Solutions :- cons Expr Hf Tf, Instances Hf Whis, w_solutions Instances Tf Wtis, w_combine Whis Wtis Expr Solutions, warn Expr Whis Solutions. %%%%%% %--------------------------------------- % Plan checking with knowledge and choice % (and strips-style action representation) %--------------------------------------- module KnowledgePlan. accumulate LK. accumulate Basic. accumulate Findall. %--------------------------------------- % actions are things you can do kind action type. %--------------------------------------- % % plans are structures showing how % doing a sequence of action % in the current circumstances % leads to desired effects. % (finish A G) represents the endpoint, % when A know desired facts G. % (step Circ Agent Act Add Del Subs) represents % a staged plan, that must be % executed when Circ are all true; % first Agent will do Act, resulting % in the addition of facts Add and the % deletion of facts Del, then we % continue with plan Subs. % (whatever Circ Char Fn) represents % a plan with a possible instantiation % in the current circumstances Circ. % There must be an individual x % characterized by (Char x), and % for any such x, (Fn x) is the plan % to carry out. % (find Action Plan) is an annotation % on plan Plan that indicates the scope % required for the action term Action. % (know Agent Circ Plan) represents a % stage of deliberation for agent Agent, % in which facts Circ characterize Agent's % information, and this information supports % the plan Plan. kind plan type. type finish agent -> list fact -> plan. type step list fact -> agent -> action -> list fact -> list fact -> plan -> plan. type whatever list fact -> (object -> list fact) -> (object -> plan) -> plan. type find action -> plan -> plan. type know agent -> list fact -> plan -> plan. %--------------------------------------- type describe_plan plan -> o. % (describe_plan Plan) % Always true; as a side-effect, print out % a sketchy description of Plan to the terminal. describe_plan (finish A G) :- output std_out "finish.\n". describe_plan (step Circ Ag Act Add Del P) :- term_to_string Act ActS, term_to_string Ag AgS, Z is (AgS ^ " will do " ^ ActS ^ "; "), output std_out Z, describe_plan P. describe_plan (whatever Circ Char PFn) :- pi o\ (describe_plan (PFn o)). describe_plan (find A P) :- describe_plan P. describe_plan (know A C P) :- describe_plan P. %------------ % Formulas with holes % (no vacuous quantifiers, for now). type close ui fact -> fact -> o. close (i F) F. close (u x\F) G :- !, close F G. close (u F) (sm G) :- pi o\ (close (F o) (H o), G o = (H o)::nil). %--------------------------------------- type circ plan -> list fact -> o. % (circ P Circ) % true if Circ are the circumstances % required now for P to be pursued to % success. circ (finish Ag Goals) Goals. circ (step Pre Ag Act Add Del Plan) Pre. circ (whatever Pre Char PFn) Pre. circ (know Ag Pre Plan) Pre. circ (find A Plan) Pre :- circ Plan Pre. type subplan plan -> plan -> o. % (subplan P Q) % true if Q may be the plan to be % considered next upon embarking on P. subplan (whatever _ _ PFn) (PFn O). subplan (step _ _ _ _ _ P) P. subplan (know _ _ P) P. subplan (find _ P) P. %---------------------------------------- type applies list fact -> plan -> o. % (applies Circ Plan) % true if Plan can be executed in Circ applies Facts Plan :- circ Plan Deps, entail_all Facts Deps. %---------------------------------------- type is_action action -> list fact -> list fact -> list fact -> o. % The domain will specify an inventory of action in % STRIPS representation: % (is_action A Preconditions Additions Deletions) % true if action A can be executed in a state where % Preconditions are all true, resulting in establishing % all the facts in Additions as true while terminating % all the relationships in Deletions. %---------------------------------------- type consistent plan -> o. kind check_state type. type check_plan list fact -> check_state -> plan -> o. % consistent Plan % is true if Plan actually maps out a good % argument about a successful course of deliberation, % choice and action for a group of agents. % % This involves a check to make sure that factual % dependencies are propagated through the proof % in a way that respects inferences about knowledge % and action in the domain, as with ordinary plans. % It also involves a check to make sure that the % structure of the plan faithfully reflects the % decision-making processes of an agent. This % means checking for the order of operators: % (find Act ... know Ag ... step Ag Act ...)* % (finish Ag G) % Both checks are admininstered by the check_plan % relation, which has auxiliary arguments for the % list of circumstances assumed, and a check_state % entry indicating where in the finite state % plan description we are. consistent Plan :- circ Plan Facts, message "Check plan\n", check_plan Facts ics Plan. type ics check_state. type mcs action -> check_state. type ks agent -> check_state -> check_state. type debug_pre_fail list fact -> list fact -> o. debug_pre_fail Circumstances Requirements :- member R Requirements, not (entail_one Circumstances R), !, term_to_string Circumstances CS, term_to_string R RS, String is ("Circumstances " ^ CS ^ "\nDon't support " ^ RS ^ ".\n"), output std_out String. check_plan C ics (finish A G) :- know_all A C G. check_plan C ics (finish A G) :- debug, not (know_all A C G), output std_out "Goals do not follow from context\n", debug_pre_fail C G, !, fail. check_plan _ _ (finish _ _) :- debug, output std_out "Plan finishes in wrong state\n", !, fail. check_plan C State (whatever Pre Char PFn) :- entail_all C Pre, !, pi o\ sigma c'\(union (Char o) Pre c', check_plan c' State (PFn o)). check_plan C State (whatever Pre _ _) :- debug, output std_out "Preconditions of whatever node not supported\n", debug_pre_fail C Pre, !, fail. check_plan C State (know A K P) :- know_all A C K, !, check_plan K (ks A State) P. check_plan C State (know _ Pre _) :- debug, output std_out "Preconditions of know node not supported\n", debug_pre_fail C Pre, !, fail. check_plan C ics (find A P) :- !, check_plan C (mcs A) P. check_plan C _ (find _ _) :- debug, output std_out "Find node encountered in wrong state\n", !, fail. check_plan C S (step MC Ag Act Add Del Plan) :- S = (ks Ag (mcs Act)), entail_all C MC, is_action Act Pre Add Del, entail_all MC Pre, remove Del MC Temp, !, union Add Temp C', check_plan C' ics Plan. check_plan C S (step MC Ag Act Add Del Plan) :- debug, term_to_string Act String, not (S = (ks Ag (mcs Act))), !, output std_out "Step ", output std_out String, output std_out " taken at wrong state of planning\n", fail. check_plan C (ks Ag (mcs Act)) (step MC Ag Act Add Del Plan) :- debug, term_to_string Act String, not (entail_all C MC), !, output std_out "Requirements at step ", output std_out String, output std_out " not supported\n", debug_pre_fail C MC, fail. check_plan C (ks Ag (mcs Act)) (step MC Ag Act Add Del Plan) :- debug, term_to_string Act String, !, output std_out "No action clause matches for step ", output std_out String, output std_out ".\n", is_action Act Pre Add Del, (entail_all MC Pre, term_to_string Del String2, output std_out "Deletions ", output std_out String2, output std_out " not supported\n" ; output std_out "Preconditions not supported\n", debug_pre_fail MC Pre), fail. %--------------------------------------- % % At this stage, it would be too cumbersome % to worry about search for plans, because % it would take us into the hairy business % of modal deduction. % % So we'll just have a set of plans that the % agent can consider - the proposition % % (stored_plans A1 A2 PL) % % will be true if PL is that set. Before % running any (new) agent, the predicate % % (store_consistent) % % can be used to make sure % that all these data structures are % correctly defined. Because this is a % user-level thing, the definition of consistent % has a lot of diagnostic messages to pinpoint % the place where a builtin plan may go wrong. type stored_plans agent -> agent -> list (ui (ui plan)) -> o. type plan_hyps list (ui (ui o)) -> o. type store_consistent o. store_consistent :- not (stored_plans self other PL, plan_hyps HL, pmember Pff PL Hff HL, lift2 (Pf\Hf\ (lift2 (P\H\ (H => (output std_out "Checking plan ", term_to_string P PS, output std_out PS, output std_out "\n", not (consistent P), output std_out "Plan is not consistent.\n"))) Pf Hf)) Pff Hff). %--------------------------------------- type choose plan -> action -> ui plan -> o. type change plan -> list fact -> list fact -> o. type scan plan -> ui plan -> o. % (choose Whole First Rest) % choose divides up a plan % the current stage of action and % subsequent stages of deliberation. % It's true if First is the first % action in plan Whole, and Rest % contains the suplan starting with % the specification of the acting % agent's knowledge at the following stage of % deliberation and choice. choose (step _ _ A _ _ P) Z N :- !, A = Z, scan P N. choose (whatever _ _ Pfn) A (u F) :- !, pi o\ choose (Pfn o) A (F o). choose P A N :- subplan P P', choose P' A N. scan (find A P) (i (find A P)) :- !. scan (finish A G) (i (finish A G)) :- !. scan (whatever _ _ Pfn) (u F) :- !, pi o\ scan (Pfn o) (F o). scan P N :- subplan P P', scan P' N. % (change P Add Del) % True if the first action in P could % result in facts Add being added % and facts Del being deleted from % the current state, strips-style. change (step _ _ _ Add Del _) A D :- !, A = Add, D = Del. change P A D :- subplan P P', change P' A D. %------------------------------------------ type goals plan -> list fact -> o. % (goals P G) % true if G gives the list of conditions % that P is designed to result in. goals (finish _ Gs) Gs. goals P Gs :- subplan P P', goals P' Gs. %----------------------------------------------- type common_goals list plan -> list fact -> o. % (common_goals L G) % true if G is the list of goals that % ALL the plans in L are designed to achieve. common_goals nil nil. common_goals (Plan::More) Goals :- goals Plan PGoals, pelts (g\ foreach (p\sigma l\(goals p l,member g l)) More) PGoals Goals. %----------------------------------------------- type achieves plan -> list fact -> o. % (achieves Plan Goals) % True if Plan results in quantifier-free % conditions Goals being true at the end % of the plan. achieves Plan Goals :- goals Plan Facts, entail_all Facts Goals. %----------------------------------------------- type recognition_status action -> list plan -> o. % (recognition_status Action Interpretations) % Always true, but as a side effect prints out % a little description (in verbose mode) noting % that Action has been or should be recognized % as reflecting one of the plans in Interpretations. recognition_status Action Expns :- verbose, !, output std_out "\nRecognized Possible Intention(s):\n", term_to_string Expns IT, output std_out IT, output std_out "\nbehind action ", term_to_string Action AS, output std_out AS, output std_out ".\n". recognition_status _ _. %--------------------------------------- type match_assumption (ui fact -> o) -> ui fact -> list fact -> list (we (ui fact)) -> o. % (match_assumption Assumable Constraint KB Results) % true if Results are the list of WEIGHTED matches % for Constraint that should be reported for % constraint-satisfaction plan-recognition. % Two cases are relevant: % - Each fact in KB which entails an instance of % the constraint (under the modal semantics for % knowledge suggested in Constraint) generates % a corresponding element of Results with weight % zero (no cost). % - If the constraint satisfies the predicate % ASSUMABLE, a arbitrary instance of the constraint % is included among the Results, with weight 1 % indicating that this goes beyond what is already % known. % The first case is handled in MATCH ASSUMPTION itself; % the second case is taken care of by the helper predicate % EXPAND ASSUMABLE. type expand_assumable (ui fact -> o) -> ui fact -> list (we (ui fact)) -> list (we (ui fact)) -> o. expand_assumable Assumable Ft L (w Ft 1::L) :- Assumable Ft, !. expand_assumable _ Ft nil nil :- debug, !, fits Ft Inst, term_to_string Inst X, output std_out "Plan recognition fails for unmatchable predicate \n", output std_out X, output std_out "\n". expand_assumable _ _ L L. match_assumption Assumable Ft Db Is :- all_pred_members (h\d\ match d h) Ft Db Exact, weight_all 0 Exact Weighted, expand_assumable Assumable Ft Weighted Is. %--------------------------------------- type plan_fits ui plan -> we (ui (list fact)) -> list fact -> action -> ui plan -> we plan -> o. % (plan_fits Template Constraints Goals Action Expectation Result) % true if Result is the instance of the stored plan Template % that you get by matching the circumstances required in % Template against the instances Constraints, by matching % the observed action Action against the first action in % Template, and if possible by assuming that the plan % matches Expectation as well and by assuming that the plan % contributes to the current goals, if possible. % % uses these two helper functions to handle the "if possible" % cases. type check_expectation plan -> ui plan -> int -> int -> o. type check_goals plan -> list fact -> int -> int -> o. check_expectation U Expect N N :- fits Expect U, !. check_expectation U Expect N M :- M is N + 1. check_goals U Gb N N :- goals U Goals, entail_all Goals Gb, !. check_goals U Gb N M :- M is N + 1. plan_fits Pf (w Solution N) Gb Action Expect (w U M) :- fits Pf U, check_expectation U Expect N N2, fits Solution Inst, circ U Inst, choose U Action _, consistent U, check_goals U Gb N2 M, !. %--------------------------------------- % % Alternative clauses just aimed to diagnose % bugs in plan specifications or context updating. plan_fits Pf (w Solution N) Gb Action Expect (w U N) :- debug, fits Pf U, fits Solution Inst, circ U Circ, goals U Goals, term_to_string Circ CircS, term_to_string Inst SS, term_to_string Goals GS, term_to_string Gb GbS, term_to_string Action AS, Z is "Plan recognition fails for inconsistency\nTemplate " ^ CircS ^ "\nInstance " ^ SS ^ "\nGoals " ^ GS ^ "\nExpectation " ^ GbS ^ "\nAction " ^ AS ^ "\n\n", output std_out Z, !, fail. plan_fits Pf (w Solution N) Gb Action Expect (w U N) :- debug, fits Pf U, fits Solution Inst, circ U Circ, consistent U, goals U Goals, term_to_string Circ CircS, term_to_string Inst SS, term_to_string Goals GS, term_to_string Gb GbS, term_to_string Action AS, Z is "Plan recognition fails for goal conflict\nTemplate " ^ CircS ^ "\nInstance " ^ SS ^ "\nGoals " ^ GS ^ "\nExpectation " ^ GbS ^ "\nAction " ^ AS ^ "\n\n", output std_out Z, Circ = Inst, output std_out "1\n", entail_all Goals Gb, output std_out "2\n", choose U R _, output std_out "3\n", term_to_string R RS, output std_out RS, output std_out "\n", choose U Action _, fail. %--------------------------------------- type rh list (ui (ui plan)) -> list fact -> list fact -> (ui fact -> o) -> action -> ui plan -> list (we plan) -> o. % (rh Templates Knowledge Goals Assume Action Expect Results) % recognition helper % % true if Results represent the instantiations of Templates % that are consistent plans whose first action is Action and % that fit a context specified by Knowledge & extensible % by the Assume predicate. % Each Result is associated with a COST that reflects % the extent to which the Result requires additional assumptions % about the acting agent, does not lead to the goals that we % know the acting agent has, or does not fit the expectations % that we have for the acting agent at this stage of the % interaction. rh nil _ _ _ _ _ nil. rh (Pff::Pffs) Db Gb Assumable Action Expect Plans :- fits Pff Pf, fits Pf Temp, choose Temp Action _, !, lift2 circ Pf Constraints, w_solutions (c\i\ match_assumption Assumable c Db i) Constraints PSolutions, filterpreda PSolutions (s\u\ plan_fits Pf s Gb Action Expect u) Plans More, rh Pffs Db Gb Assumable Action Expect More. rh (Pf::Pfs) Db Gb Assumable Action Expect Plans :- rh Pfs Db Gb Assumable Action Expect Plans. %--------------------------------------- type recognize agent -> list fact -> (ui fact -> o) -> action -> ui plan -> list plan -> o. % (recognize % Actor Beliefs Assumable Action Expect Interpretations) % True if Interpretations gives the set of plans % which the partner of Actor - Other - might attribute % to Actor upon observing Action in a context where the % intention Expect is expected, where Beliefs describes % Other's information, and where Assumable describes the % assumptions that Other is willing to make about Actor % to make Action intelligible. recognize Actor Beliefs Assumable Action Expect Interpretations :- partner Actor Other, stored_plans Actor Other Pfs, goal_desc Actor Beliefs Gb, rh Pfs Beliefs Gb Assumable Action Expect All, best All Best, filterpreda Best unweight Interpretations nil. %--------------------------------------- type recognize_as_intended agent -> list fact -> (ui fact -> o) -> plan -> ui plan -> o. % (recognize_as_intended % Actor Beliefs Assumable Plan Expect) % True if Actor's partner Other must recognize % the first action performed in Plan unambiguously to be % part of Plan by applying the information in Beliefs, % taking on assumptions as specified by Assumable, and % reasoning about the expectation for the interaction % given by Expect. recognize_as_intended Actor Beliefs Assumable Plan Expect :- partner Actor Other, know_desc Other Beliefs Kb, choose Plan Action _, recognize Actor Kb Assumable Action Expect Result, recognition_status Action Result, Result = Plan :: nil. recognize_as_intended Actor Beliefs Assumable (finish A G) Expect :- lift1 (y\ y = (finish A G)) Expect. %%%%%% %--------------------------------------- % Simulation Loop for an Agent with Collaborative Intentions. %--------------------------------------- module CollabAgent. accumulate KnowledgePlan. accumulate Findall. %--------------------------------------- % % As always we'll record the agent's % history in state data structures. kind state type. type start state. type do action -> state -> state. type see action -> state -> state. %--------------------------------------- % % Meta-actions described here. type ok action. %--------------------------------------- % Interact with the world % (via side effects). type observe state -> action -> o. observe State Action :- output std_out "What action does OTHER do?\n", input_line std_in ActString, string_to_term ActString Action. %--------------------------------------- type execute state -> action -> o. execute State Action :- output std_out "Agent performs action ", term_to_string Action AS, output std_out AS, output std_out ".\n\n". %--------------------------------------- % Determine how the context should be % updated after an action. A poor implementation for % now, whose basic idea is that % if the action is recognized unambiguously, % and just adds stuff to the context, % create an update that adds what it adds; % otherwise ask the user. % % For the future, needs to be extended to handle % - accommodation and implicit effects % - recognized plans with assumptions or % effects that we can't take on. kind percept type. type keep percept. type revise list fact -> percept. type delete fact -> percept -> percept. type extend fact -> percept -> percept. type perceive state -> list plan -> percept -> o. type deal list fact -> percept -> o. deal nil keep. deal (A::As) (extend A P) :- deal As P. perceive State (IntendedInterpretation :: nil) Percept :- change IntendedInterpretation Add nil, deal Add Percept, status "Assuming default context change.\n", !. perceive State Plans Percept :- output std_out "What context change should be inferred?\n", output std_out "(For no change: say keep)\n", input_line std_in PString, string_to_term PString Percept. %--------------------------------------- % Assumability predicates for plan recognition. type is_private_belief ui fact -> o. type is_personal_belief ui fact -> o. is_private_belief FL :- fits FL (k other Z), not (describes all Z). is_personal_belief FL :- fits FL (k self Z), not (describes all Z). %--------------------------------------- % % Predicates describing deliberation. % At each point, the agent has a % history and its intentions for the future. type simulate state -> o -> o. type think state -> o. type perform state -> list fact -> list fact -> plan -> o. type update_beliefs list fact -> percept -> list fact -> o. type update_desires list fact -> list plan -> list fact -> list fact -> o. type reconcile_intent ui plan -> list plan -> ui plan -> o. type update_intent list fact -> list fact -> ui plan -> plan -> o. type bdi state -> list fact -> list fact -> ui plan -> o. % Agent simulation involves carrying out a % Perception, % Deliberation, % Action % loop. % ! here keeps time flowing forward. think (see Action State) :- bdi State Beliefs Desires Expectation, recognize other Beliefs is_private_belief Action Expectation Expns, recognition_status Action Expns, perceive (see Action State) Expns Percepts, update_beliefs Beliefs Percepts NewBeliefs, update_desires Desires Expns NewBeliefs NewDesires, reconcile_intent Intention Expns RI, update_intent NewBeliefs NewDesires RI NewIntention, !, perform (see Action State) NewBeliefs NewDesires NewIntention. % ! here keeps time flowing forward. perform State Beliefs Desires Intention :- choose Intention Action Next, !, execute State Action, perceive (do Action State) (Intention::nil) Percepts, update_beliefs Beliefs Percepts NewBeliefs, update_desires Desires nil NewBeliefs NewDesires, (bdi (do Action State) NewBeliefs NewDesires Next => simulate (do Action State) (entail_one NewBeliefs done)). perform State Beliefs Desires _ :- execute State ok, (bdi (do ok State) Beliefs Desires (u x\i x) => simulate (do ok State) (entail_one Beliefs done)). % ! here keeps time flowing forward. simulate State Stop :- Stop, !. simulate State _ :- observe State Action, !, think (see Action State). type run o. type init_kb list fact -> o. type init_goal list fact -> o. type init_intent ui plan -> o. run :- init_kb Beliefs, init_goal Desires, init_intent Plan, (bdi start Beliefs Desires Plan => simulate start fail). % To determine your new beliefs: % - add in to what you knew before, if this is an extension % (provided you don't know it already) % - otherwise replace what you know with your percepts. update_beliefs All keep All. update_beliefs Old (revise New) All :- make_known self New All. update_beliefs Old (delete New P) All :- remove_elt New Old Next, update_beliefs Next P All. update_beliefs Old (extend New P) All :- member New Old, !, update_beliefs Old P All. update_beliefs Old (extend New P) All :- update_beliefs (New :: Old) P All. % To determine your new desires: % - add to your desires all the desires you infer % from your partner % - eliminating all those that are already satisfied. update_desires Desires Expns Beliefs NewDesires :- common_goals Expns NewGoals, union NewGoals Desires PND, pelts (g\ not (entail_one Beliefs g)) PND NewDesires. % To determine your new intentions: % - continue with what you were doing, if it's working, % - explain why you can't if something's wrong % - try something else, otherwise. type report_decision plan -> o. report_decision P :- verbose, !, output std_out "Agent decides ", describe_plan P. report_decision P. update_intent Facts Goals Plan Instance :- fits Plan Instance, applies Facts Instance, choose Instance _ _, recognize_as_intended self Facts is_personal_belief Instance Plan, status "Agent continues to act by plan.\n". update_intent Facts Goals Plan Next :- lift2 (p\w\sigma c\sigma f\ (circ p c, member f c, strip_ks f w)) Plan Problem, not (sigma i\ (fits Problem i, entail_one Facts i)), close Problem Misconception, term_to_string Misconception PS, OS is ("Agent could correct misconception " ^ PS ^ ".\n"), status OS, entail_one Facts (incorrect Misconception), stored_plans self other Alternatives, member Planff Alternatives, fits Planff Planf, fits Planf Next, achieves Next (k all (incorrect Misconception) :: nil), applies Facts Next, consistent Next, term_to_string Next NS, OS2 is ("Agent considers plan " ^ NS ^ ".\n"), status OS2, recognize_as_intended self Facts is_personal_belief Next (u P\i P), report_decision Next. update_intent Facts (GL :: Goals) Plan Next :- stored_plans self other Alternatives, term_to_string GL PS, OS is ("Agent considers goal " ^ PS ^ ".\n"), status OS, member Planff Alternatives, fits Planff Planf, fits Planf Next, achieves Next (GL :: nil), applies Facts Next, consistent Next, term_to_string Next NS, OS2 is ("Agent considers plan " ^ NS ^ ".\n"), status OS2, recognize_as_intended self Facts is_personal_belief Next (u P\i P), report_decision Next. update_intent Facts Goals Plan Instance :- fits Plan Instance, applies Facts Instance, not (choose Instance _ _), recognize_as_intended self Facts is_personal_belief Instance Plan, status "Agent finishes plan as expected and waits.\n". % For now: % - forget about what you were doing and % do what the person just asked you for. reconcile_intent _ (P::nil) N :- choose P _ N. %%%%%% %--------------------------------------- % Test domain. %--------------------------------------- module A7. accumulate CollabAgent. %--------------------------------------- % Objects include words and things. % The "semantic" relationships between % them are given by these relationships: % o_name thing noun % ta_name act-type transitive-verb kind object type. type o_name object -> object -> fact. type ta_name (object -> action) -> object -> fact. %--------------------------------------- % Rituals of conversation %--------------------------------------- %--------------------------------------- % OK is_action ok nil nil nil. %--------------------------------------- % Hello type hello action. type greeting fact. type greeted fact. is_action hello nil (k all greeting::nil) nil. is_action hello (k all greeting::nil) (k all greeted::nil) nil. %--------------------------------------- % Bye type bye action. is_action bye nil (k all done::nil) nil. %--------------------------------------- % Yes/No questions and answers. % The answer, as always, is just % looked up in the agent's information; % for the demonstration, it suffices % that the question is identified by number. kind question type. type q int -> question. %--------------------------------------- % Ask type ask question -> action. type want question -> fact. % if you ask, we know you want the answer is_action (ask Q) nil ((k all (want Q))::nil) nil. %--------------------------------------- % Answer type reply question -> object -> action. type no object. type yes object. type mmm object. type answer question -> object -> fact. type c_yes object. type c_no object. % to reply with a word communicates that the corresponding % answer is true is_action (reply Q A) (k all (want Q)::answer Q O::k all (o_name O A)::nil) ((k all (answer Q O))::nil) nil. %--------------------------------------- % Assertion type assert fact -> action. % assertion just puts a true fact on the record, for convenience. is_action (assert F) (F::nil) (k all F :: nil) nil. %--------------------------------------- % Instruction type instruct object -> object -> action. type obl action -> fact. % lambda-prolog complains at constraint-satisfaction time % if we use the built-in application here. type act (object -> action) -> object -> action. % giving an instruction of the form Verb Noun % communicates an obligation to perform the % act with the act-type denoted by the Verb and % the object denoted by the Noun. is_action (instruct AU OU) (k all (o_name O OU) :: k all (ta_name AF AU) :: nil) (k all (obl (act AF O)) :: nil) nil. %--------------------------------------- % Lexicon % Transitive verbs - type open object. type turn object. type slide object. % Noun phrases - type rightbolt object. type leftbolt object. type bolt object. type window object. type door object. %--------------------------------------- % World knowledge % Objects - type o_door1 object. type o_obj2 object. type o_window3 object. type o_bolt1 object. type o_bolt2 object. type o_bolt3 object. type none object. % States - type possible action -> A -> fact. type f_open object -> fact. type f_locked object -> fact. type f_closed object -> fact. % Actions - type a_open object -> action. type a_turn object -> action. type a_slide object -> action. % Opening something achieves openness is_action (act a_open X) (possible (act a_open X) none :: nil) (k all (f_open X) ::nil) (possible (act a_open X) none :: nil). % Turning something may lock it is_action (act a_turn X) (possible (act a_turn X) Y :: nil) (k all (f_locked Y) ::nil) (possible (act a_turn X) Y :: nil). % Sliding something may lock it is_action (act a_slide X) (possible (act a_slide X) Y :: nil) (k all (f_locked Y) ::nil) (possible (act a_slide X) Y :: nil). %%%%%% %--------------------------------------- % COMMUNICATIVE KNOWLEDGE % Precompiled plan data structures that % are logical consequences of the % theory of action and communication % that immediately precedes this. %--------------------------------------- stored_plans Self Other ( %--------------------------------------- % QUESTIONS % If the asker knows that the other % knows the answer to Q and can identify the answer, % the asker performs (ask Q); % Consequently, however W the respondent identifies % the answer, the respondent performs (reply Q w); % As a result, we achieve mutual knowledge about Q. %--------------------------------------- (u Q\ (i (i (find (ask Q) (know Self ((k Self (sm x\ (k Other (answer Q x):: (sm n\ k all (o_name x n)::nil)::nil)))::nil) (step ((k Self (sm x\ (k Other (answer Q x):: (sm n\ k all (o_name x n)::nil)::nil)))::nil) Self (ask Q) (k all (want Q) :: nil) nil (whatever (k all (want Q):: (sm x\ (k Other (answer Q x) :: (sm n\ k all (o_name x n)::nil)::nil)):: nil) (x\ (k Other (answer Q x):: (sm n\ k all (o_name x n)::nil)::nil)) a\ (whatever (k all (want Q):: k Other (answer Q a) :: (sm n\ k all (o_name a n)::nil) :: nil) (n\ k all (o_name a n)::nil) w \ (find (reply Q w) (know Other (k Other (k all (want Q)):: k Other (answer Q a) :: k Other (k all (o_name a w)) :: nil) (step (k all (want Q) :: answer Q a :: k all (o_name a w) :: nil) Other (reply Q w) (k all (answer Q a) :: nil) nil (finish all (k all (want Q):: k all (answer Q a)::nil) )))))))))))) :: %--------------------------------------- % ANSWERS TO QUESTIONS % When the respondent performs (reply Q w), % we achieve mutual knowledge about Q. %--------------------------------------- (u Q\ (i (u A\ (i (find (reply Q W) (know Self (k Self (k all (want Q)):: k Self (answer Q A) :: k Self (k all (o_name A W)) :: nil) (step (k all (want Q) :: answer Q A :: k all (o_name A W) :: nil) Self (reply Q W) (k all (answer Q A) :: nil) nil (finish all (k all (want Q):: k all (answer Q A)::nil) )))))))) :: %--------------------------------------- % ASSERTIONS % If the speaker knows G, the % speaker may (assert G); % as a result, G is shared knowledge. %--------------------------------------- (u G\ (i (i (find (assert G) (know Self (k Self G :: nil) (step (G::nil) Self (assert G) (k all G :: nil) nil (finish all (k all G::nil)))))))) :: %--------------------------------------- % REAL-WORLD ACTION % If the agent knows (act Act Object) is possible, % the agent may perform (act Act Object) % with the immediate result that facts Add % come to be true, and leading ultimately % to the satisfaction of goal Goal % SUBJECT to a PROVISO, to be enforced at % plan-recognition time, that the Act does % accomplish Add immediately and then will % achieve Goal. %--------------------------------------- (u Act \ u Object \ (i (u Add \ (u Goal \ u Parm \ (i (find (act Act Object) (know Self (k Self (possible (act Act Object) Parm) :: nil) (step (possible (act Act Object) Parm :: nil) Self (act Act Object) Add (possible (act Act Object) Parm :: nil) (finish all (k all Goal :: nil)))))))))) :: %--------------------------------------- % INSTRUCTIONS FOR REAL-WORLD ACTION % If the speaker knows the hearer knows % (act Act Object) is possible, % the speaker may perform % instruct Verb NP % provided it's also shared that Verb % refers to Act and NP refers to Object. % Then the respondent may in fact perform % (act Act Object), with the immediate % result that facts Add will come to be true, % leading ultimately % to the satisfaction of goal Goal % Again SUBJECT to a PROVISO, to be enforced at % plan-recognition time, that the Act does % accomplish Add immediately and then will % achieve Goal. %--------------------------------------- (u AU\ (u OU\ (i (u Add\ (u Goal\ (u Parm\ (u AF\ (u O\ (i (find (instruct AU OU) (know Self (k Self (k all (o_name O OU)) :: k Self (k all (ta_name AF AU)) :: k Self (k Other (possible (act AF O) Parm)) :: nil) (step (k all (o_name O OU) :: k all (ta_name AF AU) :: k Other (possible (act AF O) Parm) :: nil) Self (instruct AU OU) (k all (obl (act AF O)) :: nil) nil (find (act AF O) (know Other (k Other (possible (act AF O) Parm) :: nil) (step (possible (act AF O) Parm :: nil) Other (act AF O) Add (possible (act AF O) Parm :: nil) (finish all (k all Goal :: nil))))))))))))))))) :: %--------------------------------------- % A first HELLO % Speaker says hello, expecting hearer % to say hello in response, as a result % accomplishing a greeting %--------------------------------------- (i (i (find hello (know Self nil (step nil Self hello (k all greeting :: nil) nil (find hello (know Other (k Other (k all greeting)::nil) (step (k all greeting::nil) Other hello (k all greeted :: nil) nil (finish all (k all greeted::nil)))))))))) :: %--------------------------------------- % A second HELLO % Speaker says hello during a greeting, as % a result accomplishing the greeting %--------------------------------------- (i (i (find hello (know Self (k Self (k all greeting)::nil) (step (k all greeting::nil) Self hello (k all greeted::nil) nil (finish all (k all greeted::nil))))))) :: %--------------------------------------- % GOODBYE % Speaker says bye, indicating that the % conversation is over. %--------------------------------------- (i (i (find bye (know Self nil (step nil Self bye (k all done :: nil) nil (finish all (k all done::nil))))))) :: %--------------------------------------- % A default ACKNOWLEDGMENT % Speaker says OK, accomplishing nothing. %--------------------------------------- (i (i (find ok (know Self nil (step nil Self ok nil nil (finish all nil)))))) :: nil). %--------------------------------------- % An added database of information to take % into account when verifying that these % plans are in fact theorems -- mostly % allowing us to abstract out the physical % actions by including appropriate % universal definitions.... plan_hyps ((u Q\(i (i vacuous_assumption))) :: (u Q\(i (u A\i vacuous_assumption))) :: (u G\(i (i vacuous_assumption))) :: (u Act\ u Object\ (i (u Add\ (u Goal\ u Parm\ (i (is_action (act Act Object) (possible (act Act Object) Parm::nil) Add (possible (act Act Object) Parm::nil), entail_one Add (k all Goal), (pi X\pi Y\ union X Add Y => union Add X Y))))))) :: (u AU\u OU\ (i (u Add\ (u Goal\ u Parm \ (u AF\ (u O\ (i (is_action (act AF O) (possible (act AF O) Parm::nil) Add (possible (act AF O) Parm :: nil), entail_one Add (k all Goal), (pi X\pi Y\ union X Add Y => union Add X Y))))))))) :: (i (i vacuous_assumption)) :: (i (i vacuous_assumption)) :: (i (i vacuous_assumption)) :: (i (i vacuous_assumption)) :: nil). %--------------------------------------- % What we know to start out. init_kb ((k self (answer (q 1) c_no)) :: (k self (answer (q 2) c_yes)) :: (k self (answer (q 3) c_no)) :: (k self (incorrect (sm a\ (k self (answer (q 4) a)::nil)))) :: (k all (o_name c_no mmm)) :: (k all (o_name c_yes mmm)) :: (k all (o_name c_no no)) :: (k all (o_name c_yes yes)) :: (k all (sm a\ (k self (answer (q 1) a)) :: (sm n\ k all (o_name a n)::nil) :: nil)) :: (k all (sm a\ (k self (answer (q 2) a)) :: (sm n\ k all (o_name a n)::nil) :: nil)) :: (k all (sm a\ (k self (answer (q 3) a)) :: (sm n\ k all (o_name a n)::nil) :: nil)) :: (k all (sm a\ (k other (answer (q 5) a)) :: (sm n\ k all (o_name a n)::nil) :: nil)) :: (k all (o_name o_door1 door)) :: (k all (o_name o_window3 window)) :: (k all (o_name o_bolt1 bolt)) :: (k all (o_name o_bolt2 bolt)) :: (k all (o_name o_bolt3 bolt)) :: (k all (o_name o_bolt1 rightbolt)) :: (k all (o_name o_bolt3 leftbolt)) :: (k all (ta_name a_open open)) :: (k all (ta_name a_turn turn)) :: (k all (ta_name a_slide slide)) :: (k all (possible (act a_open o_door1) none)) :: (k all (possible (act a_slide o_bolt1) o_door1)) :: (k all (possible (act a_slide o_bolt2) o_obj2)) :: (k all (possible (act a_turn o_bolt3) o_window3)) :: (k self (incorrect (sm a\(possible (act a_slide o_bolt3) a :: nil)))) :: (k self (incorrect (possible (act a_slide o_bolt3) o_window3))) :: nil). %--------------------------------------- % We start out wanting to know the % answer to question #5 init_goal (k all (answer (q 5) Z) :: nil). %--------------------------------------- % We start out with no expectation of % how our conversational partner will % engage us. init_intent (u x\ i x). %%%%%% %-------------------------------------------------- % % This conversational agent can be run in two modes: % normal and verbose. In verbose mode, the program % prints out information about the plan-recognition % process of interpretation. In normal mode, it just % answers. % % The file illustrates the following features. % - adjacency pairs, including rituals % > hello. % hello. % - literal response based on plan reasoning & cooperation % > ask (q 1). % reply (q 1) no. % - same knowledge for generation and interpretation % > ok. % ask (q 5). % > reply (q 5) whatever. % ok. % - "helpful" responses when plan reasoning goes wrong % > ask (q 4). % assert (incorrect (sm a\ ...)). [= I don't know] % - constraint-based reference resolution % > instruct open door. % [agent performs a_open o_door1] % - plan recognition - including reference resolution - % based on known domain goals % > assert (g other (f_locked o_door1)). % ok. % > instruct slide bolt. % [agent performs a_slide o_bolt1] % % NOTE - if you want to keep talking sensibly after % this, you should really specify the following % context change when prompted after phys action % % extend (k all (f_locked o_door1)) % (delete (k all (g other (f_locked o_door1))) % (delete (k all (possible (act a_slide o_bolt1) o_door1)) % keep)). % % In other words, we know you can't slide any more, % because you did it, and we know that the sliding % worked, and therefore your goal is gone because satisfied. % ALSO, this specification all needs to be on one line! % % - persistence of cooperative goals and multiple features % in combination % > assert (g other (f_locked o_window3)). % ok. % > instruct slide leftbolt. % assert (incorrect ...) [= That bolt doesn't slide] % > ok. % [agent performs a_turn o_bolt3] % % Interestingly, this dialogue fails: % % > assert (g other (f_locked o_window3)). % ok. % > instruct slide bolt. % % for classic confusion over conflicting defaults: should I % assume that this is an instruction to do something possible, % just unrelated to your current goal; or should I assume that % this is an instruction about achieving your current goal in % an impossible way? Right now there's no preference.