{'fraction_non_alphanumeric': 0.02946259220231823, 'fraction_numerical': 0.005100105374077977, 'mean_word_length': 4.540868752919197, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 1, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Towards Cognitive-and-Immersive Systems: Experiments in a Shared (or common) Blockworld Framework

As computational power has continued to increase, and sensors have become more accurate, the corresponding advent of systems that are cognitive-and-immersive (CAI) has come to pass. CAI systems fall squarely into the intersection of AI with HCI/HRI: such systems interact with and assist the human agents that enter them, in no small part because such systems are infused with AI able to understand and reason about these humans and their beliefs, goals, and plans. We herein explain our approach to engineering CAI systems. We emphasize the capacity of a CAI system to develop and reason over a"theory of the mind"of its humans partners. This capacity means that the AI in question has a sophisticated model of the beliefs, knowledge, goals, desires, emotions, etc. of these humans. To accomplish this engineering, a formal framework of very high expressivity is needed. In our case, this framework is a \textit{cognitive event calculus}, a partciular kind of quantified multi-modal logic, and a matching high-expressivity planner. To explain, advance, and to a degree validate our approach, we show that a calculus of this type can enable a CAI system to understand a psychologically tricky scenario couched in what we call the \textit{cognitive blockworld framework} (CBF). CBF includes machinery able to represent and plan over not merely blocks and actions, but also agents and their mental attitudes about other agents.


Introduction
In contemporary research communities and industry, when agents are discussed for decision support, most of the typical use-cases are around an agent helping a single person that they are assisting. However, there are a large number of human activities in the business and enterprise world that are social, i.e., where a group of people are working together to solve a problem. Examples are: hiring a person at a company, tackling an emergency crisis like a water pipeline break, planning a medical operation, deciding on mergers and acquisitions, etc. Motivated by such applications, we are interested in how an agent -embedded in a social collaboration environment like an immersive room -can help the participants.
We introduce first the notion of a Cognitive-and-Immersive System (CAIS), which is comprised of three sub-Copyright c 2017, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.  Figure 1. The first area is responsible for perception and sensing within the environment of the human agents within the room via a range of sensors. The second area covers interpreting, understanding and acting upon that data through means such as planning, reasoning, learning, and NLP. The third area is then devoted to displaying this data in a rich visual and audio setup. The CAIS additionally has access to a variety of external machines and services that can be called upon to process requests, queries and tasks, incorporating their results. An important part of the CAIS is that there's are some number of overseeing AIs operating at the system level that can make use of any part of the CAIS to assist and aid for the humans and other AIs that are operating within the room. As a basic step, such an overseeing AI needs to be able to track the mental states of participants so that it can reason when its intervention is needed and explain if asked. While parts of this problem have been shown, we tackle this problem in such an AI system.
Within this paper, we first establish a formalization that can be used successfully within a CAIS to model the room as well as contained agents. We then define a framework for a domain of problems that can be built in a CAIS. From there, we define two tasks to test the system and show its capacity to track changing mental states during a session of use.

Cognitive Immersive Room
In development of this system, much work has gone into the creation of a Cognitive Immersive Room (CIR) which allows for research into augmenting human group collabo-ration and decision-making. To implement the CAIS cycle, the room is made up of microphones picking up people talking in the room and issuing commands to the system, the IBM Watson Conversations service parsing these commands into intents and associated entities for the intent, an executor registering the intent and acting upon it, and then projectors displaying output to the user. In addition, some actions will illicit a verbal response from the system. The executor in executing an action primarily will call out to other services (such as a name resolver to recognize people's names when they introduce themselves to the system), pushing content to the displays, or open a new display view on the projectors (or some combination of the three).

Related Work
We first discuss recent work on anticipating and modeling the mental states of humans in relation to the integrated AI systems that interact with and assist them. Specifically, work in the field of human-robot teaming has focused on the use of automated planning techniques to take human goals and (mental) states into account. Work on human-aware task planning for mobile robots (Cirillo, Karlsson, and Saffiotti 2009) used predicted plans for the humans in the system to guide the automated system's own planning process. This was made more explicit in work on coordinating the goals and plans of humans and robots (Talamadupula et al. 2014;Chakraborti et al. 2015), where a subset of the humans' mental state relevant to the autonomous system's planning problem was explicitly represented and reasoned with. Currently, very recent work has focused on adapting these previous ideas and techniques to proactive decision making (Sengupta et al. 2017;Kim and Shah 2017) and smart room environments ).
On the other hand, while these papers feature some level of formalization of mental states, they lack the necessary machinery to accomplish various tasks pertaining to a full theory of mind (Frith and Frith 2005). To do this, we consider the work done to examine how to show "selfconsciousness" (Bringsjord et al. 2015) within robot agents and how that can be mapped into formalization of mental states within humans and employed in tasks of theory of mind, such as in (Arkoudas and Bringsjord 2008). These models have been shown to be useful then in fields where AI agents have to communicate or influence other AI and human agents (Arkoudas and Bringsjord 2009).

The Cognitive Event Calculus
To capture the room in a formal way, we employ the Cognitive Event Calculus (CEC). The CECis a subset of the DCEC * , dropping the deontic operators (see (Bringsjord and Govindarajulu 2013) for the full formal definition), and is a multi-sorted quantified modal with a well-defined syntax and proof calculus. The proof calculus is based on natural deduction (Gentzen 1964), and features all of the rules of introduction and elimination that are present within first-order logic, as well as adding in rules for the modal operators. 1 Figure 2: The CECsyntax At the core of the CECis the event calculus which allows for a formalism of representing events and their effects on the world. A detailed presentation of the event calculus can be found in (Mueller 2014).
On top of the EC is the intensional operators to capture cognitions of agents. The operator B(a, t, φ) represents that agent a at time t believes φ. The operator K(a, t, φ) represents that agent a at time t knows φ. The operator D(a, t, φ) represents that agent a at time t desired φ. The operator C(t, φ) represents that at time t, φ is commonsense (and subsequently that all agents know it). The operator S(a, b, t, φ) which represents that agent a told agent b φ at time t. Alternatively, it can be used as S(a, t, φ) which represents that agent a at time t said φ (and everyone hears it). We then have the operator P(a, t, φ) which represents that agent a at time t perceived φ (giving us also that agent a knows φ at time t).
While first-order logic is an extensional system, modal logics are intensional systems. CEC is intensional in the sense that it includes intensional operators. 2 Formal systems that are intensional are crucial for modeling theoryof-mind reasoning. One simple reason is that using plain first-order logic leads to unsound inferences as shown below. In the inference below, we have an agent r, representing a CIR, that knows the manager of a team is the most responsible person in the team. Agent r does not know that Moe is the manager of the team, but it's true that Moe is the manager. If the knowledge operator K is a simple firstorder predicate, we get the proof shown below, which produces a contradiction (that r knows that Moe is the manager) from sound premises. This unsoundness persists even with more robust representation schemes in extensional logics (Bringsjord and Govindarajulu 2012).

Reasoner (Theorem Prover)
The core theory-of-mind reasoning is performed through a quantified modal logic theorem prover, ShadowProver, using a technique called shadowing to achieve speed without sacrificing consistency in the system. While describing the details of the reasoner are beyond the scope here, we give a brief overview below.
Traditionally, first-order modal logic theorem provers that can work with arbitrary inference schemata are built upon first-order theorem provers. They achieve the reduction to first-order logic via two methods. In the first method, modal operators are simply represented by first-order predicates as in the example shown above. This approach is the fastest but can quickly lead to well-known inconsistencies as demonstrated. In the second method, the entire proof theory is implemented intricately in first-order logic, and the reasoning is carried out within first-order logic. Here, the firstorder theorem prover simply functions as a general-purpose declarative programming system. This approach, while accurate, can be excruciatingly slow. We use a different approach, in which we alternate between calling a first-order theorem prover and applying modal inference schemata. When we call the first-order prover, all modal atoms are converted into propositional atoms (i.e., shadowing), to prevent substitution into modal contexts. This approach achieves speed without sacrificing consistency. 3 A Theory-of-Mind Reasoning Example Figure 3 shows a simple theory of mind reasoning task solved by the reasoner. The input assumptions state that Moe knows that engineer1 knows that if a customer has complained about a thing, then that thing needs to be tested and certified. Moe also knows that engineer1 knows that if anything needs to be tested or cleaned, one needs to request more time for that item. Finally, Moe knows that engineer1 knows that if an item is complete, one cannot request more time for it. From this, the reasoner can infer that Moe knows that engineer1 knows that if a customer complains about a thing, then that thing is not complete in around 452ms.

Planner
Spectra is a planner that builds upon the Shadow Prover. Unlike classical provers, Spectra can represent a state as any ar-3 The prover is available in both Java and Common Lisp and can be obtained at: https://github.com/naveensundarg/ prover. The underlying first-order prover is SNARK available at: http://www.ai.sri.com/˜stickel/snark.html. bitrary formula, and not just as a set of propositional atoms. Spectra can use modal formula such as "John believes everyone has left the room" in its state. Spectra can also have arbitrary formulae as its goal, e.g., "No two blocks on the table should be of the same color." The planner can also use a knowledge base of the world to work with more complex formulae and definitions. Spectra also includes a module for goal tracking and conflict resolution.

Cognitive Blockworld Framework
We now introduce the Cognitive Blockworld Framework (CBWF) that forms the base of our current experimentations for an instance of a CAIS. As we stated within our introduction, the CAI, and in this specific case CBWF, gives us a physical domain that we explore laying over it cognitive capabilities as we aim to assist agents operating in this domain. From the framework, we can generate specific Cognitive Blockworld Instantiations in which we declare the number of blocks/shapes, their properties, and how these blocks can be moved, as well as any agents and their possible prebeliefs or knowledge. We purposely leave the framework basic as it allows for creation of instantiations ranging from simple to increasingly complex ones, such as one described in (Johnson et al. 2016).
The CBFW is initially formed by taking the well-explored domain of blockworld, using the description in (Nilsson 1980), that has been used throughly for reasoning and planning. We use this well explored domain as its physical complexities have been explored (see (Gupta and Nau 1991)) as well as understanding on how it could be used for benchmarking in (Slaney and Thibaux 2001)  Translating this description to the CEC, we add two additional core sorts to the syntax: Block and Table. Additionally, both of these sorts are subsorts of a Surface sort which is defined as something that you can place a Block on. We add then define the following syntax to describe the world and the movements: On top of this, we make liberal use of the prover, Shad-owProver, and planner, Spectra. For any action that is taken, we employ ShadowProver to check if it's legal and allowed. Whenever the goals for the room are changed, we run Spectra to generate the list of moves that would complete the goal. We also use Spectra to check each move to see if it takes us toward our goal or not. The room will reject any move that takes us further away from a goal, and allow any that move us closer or affect unrelated blocks.
On top of this, we introduce the cognitive elements of the framework to capture the human agents who are part of the CAI. Human agents are allowed to freely enter and leave the room during a session. We add to our syntax: In: Agent → Fluent Whenever an agent is in the room, the agent always perceives where the blocks are in the world, and hear any change of goals in the room. However, while an agent is not in the room, he will be unaware of any changes in the room, either with the blocks or goals. When he returns, he will perceive the new configuration of the blocks, but will not know of the change in goals. The agents additionally know the rules of how the blocks can move, what their properties are, etc. Finally, whenever the goal state is changed and the room generates a plan, all agents in the room will have a belief that the result of that plan will be the configuration of the blocks in a future moment.

Scenario
For this initial work, we start with a very elementary CBWI. We include only three identical blocks, A, B, and C, which all start on the table. This is represented as: holds(On (A, Table), t) holds(Clear(A), t) holds(On(B, Table), t) holds(Clear(B), t) holds(On(C, Table), t) holds(Clear(C), t) There are only two human agents, Matthew and Robert, who only have knowledge about how blockworld works. Using this instantiation, we give the room two tasks to demonstrate its theory of mind.
For both tasks, we will use the following sequence of events to setup the world for the two tasks:

Modified False-Belief Task
An initial test of our framework of the models is completion of a variant of the False-Belief Task. 4 We base this on the Sally-Anne variant developed in (Baron-Cohen, Leslie, and Frith 1985) wherein a child is presented with two dolls, Sally and Anne, as well as a basket, box, and marble. With both dolls present, the marble is placed in the basket, and Sally leaves. The marble is then moved to the box, and Sally returns. The child is asked where Sally would look for the marble. To accomplish the task, the child must possess a theory of mind and be able to construct mental states for each of the dolls that contain where the marble is located. Modifying the task for our CWBI, the child is replaced by the CIR and the dolls are the human agents within the room. Parallel to the Sally-Anne example, the room must keep track of the mental states of the participants in the room and be able to reason about what the humans believe to be the room configuration and goals. However, we extend this and require that the room must also be able to step in and correct a human who makes a false-belief about the current goals of the room in an informative way. For both of these, we consider the action sequence outlined above for our two agents adding in a final step of Robert trying to move block A to the table.
For the first portion of this task, we consider the world between steps 5 & 6. At this point, we wish to see where the room believes the blocks are, as well as where it believes that Matthew and Robert think the blocks are, focusing primarily on block A. We ask the machine these three questions, translating them into the CEC: 1. "Where do you (CIR) believe block A is?" 2. "Where does Matthew believe block A is?" 3. "Where does Robert believe block A is?" We translate these sentences into the CECwhich we can then pass down to ShadowProver to answer. For each question, we convert it to an "exists" check and then parse the returned proof to find what statement unified with it to give us where block A is in the world. The exists statements for the questions are of the form ∃ x B(a, t, holds(On(A, x), t)) (where a represents the agent under question).
For the first two questions, both the AI and the agent Matthew are in the room and can perceive where the block is and thus have knowledge of its location. Robert left the room at step 4 and missed the block being moved at step 5. Therefore, his knowledge of where the block is remains at what it was when he was in the room. We show the three statements below generated from ShadowProver that answers the above questions as well as show a visual representation of this answer in Figure 4:  Table), t)) B(Matthew, t, holds(On(A, Table), t)) B(Robert, t, holds(On(A, B), t)) For the second part of the task, we consider how the room responds after step 9. As stated before, the room is setup such that it will not allow any move that it considers inefficient and takes it away from its current goals. As stated previously, while agents can perceive the location of blocks, they cannot for goals, and will miss any change in goal states while outside the room. When someone makes a move the machine deems inefficient, the room attempts to determine why the agent is making such a move by checking to see if the agent has any goals that differ from the room itself and if the plan for that goal contains the attempted move. As agent Robert still believes that the goal is On(C, B), the room detects this and that it differs from the current goal of On(A, C). From here, it runs another instance of Spectra using the current block configuration with the believed goals of the agent to determine if the move is part of the plan to achieve the goal. Determining that it is the case here (as unstacking A to the table is the first step of the generated plan), the machine knows now that agent Robert has a false-belief about the current goals of the room. The room then notifies Robert, showing a side-by-side comparison of the current goals (and the plan to achieve it) and what his goals were (and the plan to achieve them) shown in figure 5. The system is able to do this, allowing for lag due to network calls, on average in around 748ms employing ShadowProver and Spectra multiple times.

Catching People Up Task
The second task we define for our system is in assisting people catch-up when they return to the room. As previously seen, we know that Robert has missed that the goals of the room have changed, but would perceive the new configuration of blocks. Thus, similar to the previous task, he knows the location of the blocks and which are clear, but does not know that the goals have changed.
However, sensing that something is amiss with the con- Figure 5: Visual Output to Robert Showing His False Belief figuration per his believed goal, the agent should be able to query the system as to what has changed in the room while he was not in it, receiving a new updated list of goals as well as how the blocks have been reconfigured.
To handle this task, we add additional machinery to our system in not only tracking people's current mental states, but also saving the mental states at certain points of significance. We define these points as being at when a person would begin to miss information as they leave the room, saving that full mental state to memory. In the case of Robert, we say that his saved moment is p1 and is saved at step 4 and would appear as it does in Figure 4. From here, the room does two things. The first is to determine how the goals of the room have changed and the second is how the world has minimally changed. To accomplish the first step, we generate a list of goal axioms from Robert's mental state and compare it against the room's current known goals, showing the goals that have been removed and added. The next step is determining how the configuration of the room has changed. To do this, we can employ Spectra our planner. We use the axioms that describe our configuration at p1 as our initial state and the axioms at t to describe our goal state, and allow it to generate a plan on how we could have gotten there. The resulting plan is generated in around 848ms and shown back to the user where they see what changes, such as in figure 6), and allows them to update primarily what their beliefs in the goal of the system is (which the system saves in its understanding of Robert's updated mental state), and successfully completing this task.

Conclusion
We now quickly summarize our contributions and present promising future lines of work. Our primary contribution is in the creation of an overseeing AI that is capable of tracking participants' mental states as they operate within a CAIS. This AI is capable of using this information to reason and plan assisting the participants in completing a task and tracking information as well as generate explanations for its actions. As part of this system, we give a definition for a concrete framework that can be used to generate future tests of increasing complexity for the system. We give the necessary machinery via syntax and sorts to use this framework as well as show a base implementation that was derived from the framework. Within this implementation, we show two tasks that can be solved via the the overarching AI that encompasses a CAIS and has a sufficient definition of theory of mind.
Future work will be in creating additional domains of work, further empowering the overarching AI and to create an overarching formal definition for a Cognitiveand-Immersive Framework (CAIF). The Cognitive-and-Immersive Framework would form the basis for any of our cognitive frameworks, which includes the CBWF. From this core definition, we hope to expand our system to other domains that would benefit from the cognitive capabilities demonstrated here.
For one such domain, the presented work can be very useful in business negotiation scenarios like contracts management or using software where multiple parties are involved and can have different vantage points (mental models) for discussion. There has been some work on analyzing contracts for identifying gaps (Desai, Narendra, and Singh 2008) and terms of conditions for software services(Vukovic, Laredo, and Rajagopal 2014) but they do not consider parties' mental models.