Analyzing Military Intelligence Using Interactive Semantic Queries Rod Moten Data Fusion and Analytics Sotera Defense Solutions Aberdeen Proving Grounds, MD, USA rod.moten@soteradefense.com Abstract— We describe a strategy for performing semantic then the external organization and the attacking family have searches for analyzing military intelligence. Our strategy allows common interests. Or it could be inferred using network the analyst and the query engine to work together to reduce a analysis because Sadat Baba and Taliban both are linked to complex query into simpler queries. The answers for the simpler Dalazak by the same relationship within the same subgraph. queries are combined into answers for the original query. The queries can be refined using rules defined by the analyst or The current state-of-the-art for military intelligence analytics created by a data scientist. Our strategy uses an analysis focuses on the analyst using visual aids and various alternative approach to semantic modeling than the state-of-the- retrieval techniques, such as faceted search and querying, to art approaches based on OWL. OWL is an implementation of a perform this inference manually [3]. Military intelligence branch of mathematical logics designed specifically for semantic analysis systems should focus on developing strategies for modeling called description logics. Our strategy uses a branch of reducing the manual work performed by analyst by mathematical logics called type theory. We use type theory incorporating more automated methods. The effort for because of the long history of developing systems based on type searching for data can be reduced if the query engine theory for reasoning interactively. We demonstrate with an automated some of the work the analysts performed manually. example how the strategy can be used to answer questions posed This means the query engine would need to have analytics that by analysts that couldn't be answered using conventional automate some of the inductive and deductive reasoning methods. performed by the analyst. Keywords: semantic search; military intelligence; analytics; Some of the analytics used in a query or search may be type theory; ontology; semantic modeling; interactive theorem different from the analytics used in ETL (extraction, proving transformation, and load). In ETL, analytics are used primary for entity and feature extraction, entity resolution, and entity I. INTRODUCTION fusion [4]. In this case, the analytics aren't used to answer a "The Army is working closely with the intelligence query posed by an analyst. The analytics we are interested in, community and other Defense Department partners, including such as multi-relational link predication [5] [6], occur after the Navy, in developing cloud-based systems for battlefield ETL. The analytics will be performed after the data has been intelligence."[1] The goal of the U.S. Army is to fulfill theater mapped into a graph-like structure, such as RDF or DRIF [7], intelligence requirements using these systems as much as [8]. Therefore, the query engine will need the ability to express possible [2]. For example, suppose an analyst created a the behavior of the analytic in terms of the underlying semantic hypothesis that a family within an Afghan village is network. responsible for several IEDs. The analyst may use the Cloud to The behavior of an analytic can be specified as the logical determine which families have connections to hostile implication of the postcondition from the precondition. The organizations. The data may be in the Cloud that directly links precondition is a logical statement that must be satisfied in a family to a hostile organization. For example, suppose the order for the analytic to produce valid output. The Sadat Baba family [2] is a member of the village and postcondition is a logical statement that describes the intelligence data contains the triple (Sadat Baba shares-profit characteristics of the concepts and relationships produced by Taliban). In the triple, Sadat Baba is the subject, shares-profit the analytic. In the simplest case, the specification of an is the predicate and Taliban is the object. On the other hand, analytic could be defined as ! → ! , where ! is the the intelligence data may only contain data that indirectly links precondition and ! is the postcondition. For example, the the family to a hostile organization. These links have to be precondition of the analytic for associating a family and an inferred either deductively or inductively from the data. For external organization would be 'for any ? ! ∈ Family and example, it may be possible to infer that Sadat Baba and the ? ! ∈ National(Organization there exists a ? ! ∈ Family such Taliban have common interests because both Sadat Baba and that ? !!attack!? ! and ? !!attack!? ! '. The postcondition the Taliban attacked the Dalazak family. This could be inferred by applying the following rule. If a family and an external would be ' ? !!common!interests!? ! '. organization attack another family in the same tribe or village, STIDS 2013 Proceedings Page 109 The examples above may mislead the reader to believe that Their approaches use heuristics to perform inductive and first-order logic would be sufficient for expressing the deductive reasoning. They also use machine learning to find precondition and postcondition. However, first-order logic new rules to add to the knowledge base. Our strategy support doesn't support cases when analytics can operate on a set of inductive and deductive reasoning except we use proof- concepts and roles. For example, consider an analytic that uses theoretic methods used in interactive theorem provers. numeric calculations to determine relationships, such as Theorem provers, such as NuPrl [18], Coq [19], and Isabelle common neighbor algorithms [9]. Such an analytic only cares [20], use interactive methods for developing formal about relationships or edges between nodes. So it can operate mathematical proofs. In these systems, the assertions are type on any concept. For example, if the analytic uses a common judgments. Type judgments are logical statements that ask neighbors algorithm for determining the common-interests which objects belong to a specific type. The types can be relationship, then the precondition would be 'for any ? ! ∈ defined to resemble logical statements, such as ! ∧ ! → !. We ? !and ? ! ∈? ! there exists a ? ! ∈? !such that ? !!? !!? ! use this same technique in our query language. However, our and ? !!? !!? ! '. In this precondition, we parameterized the type theory differs from the state-of-the-art in order to support concepts for the attackers, Family and National Organization, semantic modeling. and we parameterized the attack relationship. We can also K-DTT [21] and S-DTT [22] are type theories that use an parameterize the postcondition. For example, a data scientist extensional approach to semantic modeling. Description logics may be able to improve the analytic to infer a stronger also use an extensional approach to semantic modeling. This relationship between the attackers using additional information means that A-Box statements or an external source, such as a about them. In this case, the postcondition would be 'there database, has to be used to determine that an object belongs to exists a ? ! ⊆ common!interests such that ? !!? !!? ! '. a concept. In TT-IQ, concept membership is intensional. In The query engine could use the specification of an analytic other words, we determine whether an object belongs to a as a rule for solving an intelligence requirement. If the concept based on how the object was constructed. Therefore specification of an analytic is ! → ! and the intelligence there is no need for A-Box statements or external sources to requirement can be reduced to !, then the solution to the determine concept membership. intelligence requirement would be the concepts and Type theory isn't the only method of using higher-order relationships that the analytic produces that satisfy !. logic for semantic modeling. Classical higher-order logics have In this paper, we present a strategy for analyzing been used for semantic modeling as well [23]–[26]. However, intelligence data using an interactive query language. When a the query languages used in these approaches do not allow a user specifies a query, the query engine solves the query by user to define analytics to be incorporated into the query refining it into new queries. If any of the new queries cannot be engine. answered, it asks the user to assist it. The user assists the query Rule-based approaches for semantic search, such as Tuple- engine by specifying an analytic or rule that can solve the Generating Dependencies [27], have the capability to query or reduce the query into new queries. This process incorporate rules specified by a user into the query answering continues until all queries are answered or until there is a query process. However, these approaches are implemented using that cannot be answered. The query engine keeps track of this first-order reasoning techniques from logic programming. As a process and combines the answers from the generated queries result, they will not be able to support domain metamodeling. into an answer for the original query. At the heart of the query Our strategy, on the other hand, will support finding concepts language is the type theory TT-IQ, Type Theory for Interactive and relationships that meet specific criteria. Querying. The query engine for TT-IQ consists of a framework that allows a data scientist to define analytics that III. INTERACTIVE QUERYING can be included in query processing and for analysts to add new rules. In this section, we give an overview of how interactive querying is performed. Interactive querying is analogous to This paper is outlined as follows. First, we present work proving a type judgment. Informally, a typing judgment related to our strategy. Then, we use an example to consists of a goal and a set of assumptions. The goal is the demonstrate interactive querying. Next we give an overview of assertion we want to prove. The assumptions represent facts TT-IQ. Finally, we conclude the paper with a discussion of our and statements from the knowledge base. Therefore, it consists strategy. of logical statements about the semantic meaning of concepts and relationships. II. RELATED WORK Fig. 1 shows an example proof created from an interactive Our strategy is similar to approaches that use a semantic query for attacks in a region that may have involved a specific network or ontology for refining queries. These approaches, person. We assume the analyst only knows that the person has such as QUICK [10], LISQL [11], and query rewriting [12] use a set of features observed by an interrogator, such as facial semantic information to enhance a query supplied by a user. marks, height, and the number of a cell phone belonging to the These approaches use a semantic network and stepwise detainee. This query is stated as a judgment that appears as the refinement to create semantic queries. Our approach, on the root of the proof tree. Here we state the judgments informally other hand, uses stepwise refinement for query execution. in natural language. The assumptions in the judgments in Fig. 1 Researchers at GMU have spent over 15 years developing contain a definition of a type representing the concepts Attack strategies that could be used for interactive querying [13]–[17]. and Person; an object representing the features of the detainee; STIDS 2013 Proceedings Page 110 Fig. 1. Example proof created from an interactive query features of the detainee; declarations of the predicate symbols, two tactics have the same rank, then the user will need to select such as involving; and definitions of data types that represent the tactic to apply. cell phone numbers and regions. The assumptions also contain a taxonomy of properties and features. The taxonomy is Narrow Predicate is similar to Narrow Concept, except Narrow Predicate replaces a predicate symbol with another defined as a partial ordering on predicate symbols and attribute names. predicate symbol. Therefore, Narrow Predicate has antecedents to prove that the replacement predicate is a sub-property of The query engine determines which tactics can be applied substituted predicate. This requires two antecedents: an based on whether the conclusion of a tactic matches the goal of antecedent to prove that the replacement property is a sub- a judgment. The query engine uses the type compatibility property of the existing property and an antecedent to prove relationship [28] of TT-IQ to perform matching. When two that the type of the sub-property is a subtype of the type of the types !and !′!are compatible, it means that an object in ! can super-property. The first antecedent has to be proved using the be converted to an object in !′ and vice versa. Type taxonomy of the properties and features. The tactic also has a compatibility is an extension of the subtyping relationship in third antecedent that contains the sub-property instead of the TT-IQ. We give an overview of subtyping in "Overview of TT- super-property. The proof tree in Fig. 1 shows the judgment IQ". produced from the third antecedent. In particular, it shows "involving" replaced with "near". Each tactic has a conclusion and zero or more antecedents. When a tactic matches a judgment, the query engine creates The judgments produced by Concept Introduction illustrate new judgments for each antecedent. For example, the Narrow the need for dependent judgments. Normally in type theory and Concept tactic is a built-in tactic that replaces a type ! in a in sequent calculus, judgments of the same parent are term with a subtype of !. This tactic has two antecedents. One independent of each other. However, when using interactive antecedent is a judgment that asserts the replacement type is a proofs to query for data, terms created on one branch could be subtype of the substituted type. The other antecedent is the used in a judgment on a different branch. Notice that two of the same as the conclusion except all occurrences of the supertype goals produced by Concept Introduction contain ≔ . This are replaced with the subtype. Fig. 1 only shows the second special constructor informs the query engine to create a antecedent because the first antecedent can be proved reference to the term that satisfies the type on the right hand automatically using TT-IQ's subtyping relationship. side of≔. At some point, a tactic will be invoked that uses an analytic to create objects or find objects in the knowledge base In practice, the query engine will only show the judgments to bind to the reference. that require assistance from the user. There may be multiple tactics that can be applied to a judgment. The compatibility The Geo Search tactic uses an analytic to bind a reference relationship can rank the tactics that match best. However, if to a collection of terms that are within a specific region. Geo STIDS 2013 Proceedings Page 111 Search uses the goal as the criteria to search for objects within Both types and objects are terms. We define the terms ! a specific region in the knowledge base. More specifically, Geo and ! as follows. Search has a conclusion that has a type that contains one attribute, location. The type of location is the supertype of all !, ! ≔ ⊥ !! !|! ! ! !! , … , !! !. ! !.size types that could be used as the criteria for a geospatial search, tt|ff !! = !! , … , !! = !! |[!! , … , !! !]!! such as KML. This type matches any type that has an attribute that is compatible with KML and the name of the attribute is !! ∧ ! ! ! ∨ ! ! ! → ! ! |¬!|! !! , … , !! prop interchangeable with location. The taxonomy determines which !! ℛ !! : !! × …×!!! : !! ! ∗ | !: !|!′ attributes are interchangeable with location. The tactic uses this attribute as the search criteria. In practice, the tactic may also |∀!: !. !′|∃!: !. !′!|∀! ≤ !. ! ! |!∃! ≤ !. ! ! |!! require a time range. Person Observation is a tactic that is created by a data In the definition of terms, ! and ! range over strings and scientist. In other words, it is an analytic that creates concepts numbers respectively; ! ranges over attribute names; and ! inductively. This means it creates the definition of a type by generalizing existing data. Let's assume that Person and ! range over variables. The term ⊥ represents null. The Observation examines SIGINT data for calls originating form terms tt and ff represent true and false, respectively. The terms or made to the telephone number of the cellphone in the of the form !! = !! , … , !! = !! represent records. Each possession of a detainee. The time and location of the each call !! = !! in a record represents an attribute where !! is the name is used as an observation point of the person. In theory, a new of the attribute and !! is the value of the attribute. The terms of triple is added to the knowledge base that links the person to the form !. ! represent selecting the value of an attribute whose the time and location of the call. In practice, the query engine name is ! from a record ! . Terms of the form [!! , … , !! !] may not create the triples. Instead, the query engine may define represent lists. Terms of the form !.size represent the number a way to create the triples on demand without altering the of elements in the list !. ! and ! range over predicate symbols knowledge base unless directly instructed to do so. This and function symbols, respectively. ! is the type of strings and approach is essential for cloud-scale data because it doesn't ℛ is the type of numbers. We call the terms ! , ! , ! , perform any destructive modifications if the analyst wants to !(!! , … , !! ) , !. ! , !.size , tt , ff , !! = !! , … , !! = !! , and back out changes. Instead the query engine could have a local [!! , … , !! !] objects. We call all of the other terms, such as cache containing the new triples. The modifications could be !: !|!′ and ∃!: !. !′, types. made permanent only when explicitly specified by the analyst Terms of the form !! : !! × ⋯×!!! : !! represent record types or a data scientist. and terms of the form ! ∗ represent list types. The type prop The antecedent and conclusion of a tactic based on an represent the type that contains types that represent logical analytic is determined by the precondition and postcondition of formulas, such as ! ∧ !′ and ! !! , … , !! . Any type created the analytic. The system uses the precondition as the using terms in prop will also be in prop. For example antecedent and the postcondition as the conclusion. For Person grt! 5,4 ∧ !grt! 7, 3 is a member of prop. Terms of the form Observation the postcondition states that there exists a concept !: !|!′ represent set types. Intuitively a set type ! where each object is a Person that has the features of the !: !|!′ !represents a list of objects of type ! where each detainee and whose locations correspond to the locations of the member of the list makes the type representing the logical cell phone. The precondition requires that there exists a person formula !′ true. We call ! a reference. We use ! to support in the knowledge base who has the features of the detainee. To injecting terms created by an analytic running in a separate satisfy the precondition, the analyst will need to add the subsystem. Notice there are two kinds of quantifiers, those that detainee to the knowledge base. The precondition also requires range over objects,!∀!: ! and ∃!: !, and those that range over that we can determine the locations of the cell phone. We types, ∀! ≤ ! and ∃! ≤ !. In the quantifiers that range over assume another analytic will determine this location. For objects, !: ! means ! is a member of type !. So, ∀!: ! means brevity, assume that the query engine can prove this for all terms ! that are members of the type ! . In the automatically. As a result, it isn't included in Fig. 1. quantifiers that range over types, ! ≤ ! means ! is a subtype We envision a suite of tactics that discover relationships of !. So, ∀! ≤ ! means for all types ! that are subtypes of !. between an entity and an event. These tactics use analytics that Notice that types may contain objects. For example, if grt can create new relationships. In other words, they can add new is a predicate symbol that represents greater than equal to and triples to the knowledge base. Nearness Predicate belongs to abs is a function symbol that represents absolute zero, then this suite. Nearness Predicate uses an analytic that creates new !: ℛ|grt abs ! , 0 is a type that contains the objects 0 and triples using the near predicate. In other words, it creates triples abs(!). of the form (! near !) where ! is an entity and ! is an event. Given any two terms ! and !′ and a variable !, ![! ! /!] is IV. OVERVIEW OF TT-IQ the term produced by replacing all free occurrences of ! in ! with !′. For example, ! ! !, ! , ! 3/! is ! ! 3, ! , 3 . For In this section, we give the formal definition of TT-IQ. Due two terms ! and !, we write !: ! to mean that ! inhabits the to space limitations, we omit some rigor that would be found in type ! or ! is a member of the type !. For example, 3: ℛ and a normal presentation of type theory. 3,4,5 : ℛ ∗ . We give some of the rules of TT-IQ for determining which terms inhabit a type in Fig. 4. STIDS 2013 Proceedings Page 112 !! ⇀ !!! ⋯ !! ⇀ !!! location:KML . Geo Search doesn't take any relationships as (REC. ⇀) input. (!! = !! , … !! = !! ) ⇀ (!! = !!! , … , !! = !!! ) Traditionally, the definition of a type theory includes rules ! ⇀ (!! = !!, … , !! = !! ) ! = !! for evaluating terms. As a result, most type theories in the (FIELD!SELECTION ⇀) literature are definitions of statistically typed functional !. ! ⇀ !! programming languages. TT-IQ has rules for evaluation. We list a subset of the rules in Fig. 2. TT-IQ should not be !! ⇀ !!! ⋯ !! ⇀ !!! considered a functional programming language. TT-IQ does !(LIST ⇀)! [!! , … , !! ] ⇀ [!!! , … , !!! ] not contain a construct for creating functions. Instead, TT-IQ defines a means for injecting functions and relations into it that ! ⇀ [!! , … , !! ] are executed by an external subsystem or programming (LIST!SIZE ⇀)! language. We represent the external subsystem or !.size ⇀ ! programming language as an interpreter. For any term !, an ℑ!!(!! , … , !! )! ↦ ! interpreter maps ! to a term !′ . We use ℑ to denote an (FUNCTION!APPLICATION ⇀)! interpreter. We write ℑ ! ↦ !′ to mean that ℑ interprets ! as !(!! , … , !! ) ⇀ ! !′ . The interpreter is used to evaluate the application of ℑ!!(!!, … , !! )! ↦ ! function symbols and predicate symbols. For a term !, we (PREDICATE!APPLICATION ⇀) write ! ⇀ !′! to mean ! evaluates to !′ . The rules !(!!, … , !! ) ⇀ ! FUNCTION!APPLICATION ⇀ and PREDICATE!APPLICATION ⇀ indicate that the application of a function symbol or a predicate symbol ℑ!!! ! ↦ ! to a sequence of terms is equal to the interpretation of the (REFERENCE ⇀)! !! ⇀ ! application of the function symbol or predicate symbol. These rules do not require that the arguments of the function symbol and predicate symbol be evaluated before passing them to the Fig. 2. Evaluation rules for terms that do not evaluate to themselves. interpreter. As a result, the interpreter can determine the mode of evaluation, such as lazy evaluation or eager evaluation. The The specification of an analytic can be generalized as evaluation rule REFERENCE ⇀ illustrates the ability of the follows. The specification will need to contain universal interpreter to manage storage of instance data. Intuitively quantifiers to allow the query engine to pass in types and REFERENCE ⇀ means that a reference to a concept evaluates to objects to the analytic. If the analytic takes in ! types and ! the set of individuals in the concept. The concept is defined by objects, then the specification will need the quantifiers the type ! and ! is a pointer to an index, graph or other data ∀!! ≤ !! . ⋯ . ∀!! ≤ !! and ∀!! : !! . ⋯ . ∀!! : !! . We structure that contains members of the concept. abbreviate these as ∀! ≤ ! and ∀!: ! , respectively. An A paramount feature of TT-IQ is subtyping. TT-IQ uses a analytic may output types and objects. If an analytic generates unique feature to typing that is required for semantic modeling. ! types and ! objects, then the specification will need to Traditionally, subtyping on record types is the same as class contain existential quantifiers ∃!! ≤ !!! ⋯ ∃!! ≤ !!! and inheritance. In other words, a record type ! is a subtype of !′ if ∃!! : !!! . ⋯ . ∃!! : !!! . We abbreviate these as ∃! ≤ ! ! and all the attributes in !′ are also attributes in !. This means that ∃!: ! ! , respectively. The specification will also contain the for every attribute named ! in !′ there is attribute ! in T. precondition and the postcondition of the analytic. We denote However, this definition of subtyping ignores the semantic these respectively as ! and !. The general term that represents meaning of attribute names. Two attributes can have different the specification of an analytic is specified in (1). names, but mean the same thing. As a result, TT-IQ defines subtyping so that attribute names do not have to be ∀! ≤ !. ∀!: !. ! → ∃! ≤ ! ! . ∃!: ! ! . ! (1) syntactically the same, but semantically the same. Actually, in TT-IQ attribute names do not need to be equivalent, but one In practice, the number of inputs and outputs of an analytic attribute name has to be subsumable by the other. The will be small. For example, the specification of Geo Search, an definition of subtyping in TT-IQ uses a partial ordering on analytic that finds objects that occur within a region, is as attribute names to define subtyping. Due to space limitations follows. we are unable to define the complete definition of subtyping. ∀! ≤ location:KML . ∀!:KML.true We do show the subtyping rule for record types below. (2) → ∃!: ! ∗ . ∀!: !.inRegion !, ! !≥! for!! = 1, … , ! !! ⊑ !′! !! ≤ !′! In the specification of an analytic, the !'s and !'s in (1) represent concepts and the !'s and !'s represent individuals. An !1 : !1 × ⋯×!! : !! ≤ !′1 : !′1 × ⋯×!′! : !′! analytic may also take relationships as input and output In "Interactive Querying" we showed examples of tactics. relationships. The relationships an analytic takes as input are A tactic is a program or script that returns a proof tree. A proof defined by !, and the relationships an analytic produces are tree represents a proof of a type judgment. Intuitively a type defined by !. For example, the Geo Search analytic outputs a judgment asserts that a term belongs to a type. A type relationship inRegion !, ! . The domain is defined by the type judgment has the form ! ⊢ !: !′ where ! represents an of ! which is KML and the range is all subtypes of environment and !: !′ represents the assertion that ! inhabits STIDS 2013 Proceedings Page 113 to prove judgments that require an analytic. ANAYLIC!EVAL generates concepts and individuals that satisfy a condition specified as a type. The condition can represent a relationship or the search criteria for a query. The condition is specified as the type ! in ANAYLIC!EVAL. An analytic whose postcondition matches ! is used to generate the concepts and individuals that satisfy the condition specified as !. In the rule, the analytic is ! and its postcondition is !. The top-right hypothesis is used to establish that ! matches ! if replacing the free variables in ! produces a term that is a supertype of !. The terms that Fig. 3. Interaction between the query engine, the rule engine, and the replace the free variables are the inputs to the analytic, ! and interpreter. !, and the outputs of the analytic, ! and !. ! is a sequence of types !! , … , !! and ! is a sequence of objects !! , … , !! . !′. The environment, !, of a type judgment consists of type Likewise ! is a sequence of types !! , … , !! and ! is a assignments, terms, predicate symbols and function symbols. It also consists of pairs of predicate symbols and attribute names. sequence of objects !! , … , !! . Intuitively, ! and ! are the These pairs form a partial ordering, ⊑. If !! , … , !! are type concepts and individuals required by the analytic to produce assignments of terms, predicate symbols, and function the concepts and individuals ! and ! that satisfy the symbols, then ⊑; !! , … , !! is an environment. relationship defined by !. All free variables in each !! and !! are declared in !. Each !! and each !! do not have any free Only the rule engine can execute a proof rule. The rule variables. engine is a subcomponent of the query engine. Given a rule, a proof tree, and judgment in the proof tree, the rule engine will Since ! and ! represent the input to the analytic, we need apply the rule to the judgment. The result will be a proof tree to verify they satisfy the precondition !. The three hypotheses that uses the antecedent of the rule to create children of the of ANAYLIC!EVAL on the left achieve this. The top two judgment. Fig. 3 illustrates the relationship between the query hypotheses are judgments to verify that the inputs to the engine, the rule engine and the interpreter. analytic have the correct types. The last of the three hypotheses TT-IQ does not define the language in which tactics are verifies that ! is true with all of its free variables replaced with written. An interpreter performs evaluation of tactics. Detailed inputs to the analytic. The top hypothesis on the right is used to discussion of the language for creating tactics is outside the verify that the postcondition is true for the inputs and outputs scope of this paper. In this paper it suffices to say that a tactic of the analytic. The second hypothesis from the top on the right takes as input a typing judgment and outputs a proof tree. The indicates that the output of ! on ! and ! produces ! and !. root of the tree has to be the input judgment. The tactic has to Recall from FUNCTION!APPLICATION ⇀ in Fig. 2 that an use proof rules to create the proof tree. interpreter is used to produce ! and !. The hypothesis on the bottom-right indicates that each !! evaluates to a list of terms Fig. 4 contains a few proof rules for TT-IQ. We use of type !! and that each !! evaluates to a term that is of type ∃! !ELIMINATION to specify that an analytic will retrieve the individuals of a concept represented as !!or a subtype of !. !!! . This hypothesis shows that we intend to represent concepts The rule uses a concept reference so that we can postpone as list of terms of a specific type. The ∃{} !REWRITE rule makes selection of the analytic until we have a judgment whose type use of the fact that for any term !, if !: !: !|! ! then !: ! and matches the postcondition of an analytic. We use ANAYLIC!EVAL !, !! ≤ ! ⊢ ![!! !/!]:prop !(∃! !ELIMINATION ) ! ⊢ ∃! ≤ !:prop ! ⊢ ∃! ≤ !. (∀!: !. ! ! ) ∧ ! !! :prop ! (∃{} !REWRITE) ! ⊢ ∃! ≤ !!: !|! ! ! ′!. ! !! :prop ! ⊢ !!⃗ ! ≤ !!!⃗ ! ! ⊢ !! ≤ ![!!!!⃗ /!!⃗ ][! !⃗ /!⃗ ] !!⃗/!⃗][!⃗/!⃗][! !⊢! !!⃗ !⃗: ! !(!!⃗ , !⃗) ⇀ !! !!!⃗ , ! !!⃗! !⃗ /!⃗ ]:prop !!!! ⇀ !! !!!"#!! ⊢ !! : !!∗ !! ⇀ !!! !!!"#!! ⊢ !!! : !!! ! ⊢ ![!⃗/!⃗][! (ANAYLIC!EVAL) !, !: ∀!⃗ ≤ ! !⃗. ∀!⃗: ! !⃗. !! → ∃! !⃗ ≤ !!!!⃗ ! ! . ∃!⃗: !!!⃗ ! ! . !!, ! ! ⊢ !:prop ! ⊢ ! ≤ ! ! ⊢ ∃! ≤ !. ! ! :prop !(NARROW!TYPE) ! ⊢ ∃! ≤ !. !′:prop! Fig. 4. A subset of the type rules of TT-IQ STIDS 2013 Proceedings Page 114 !! !!!"#$%&'!!"#$%&'(!!"#$$%&' ! !! ! !!!"#!!"#$%!&" !! ! ! !! A. Believability ! ! !!!"#$%&! ! !!!"#$%&"'! ! ! !"#$ !! ! ! !!! !! !!! !!!"#$!!! !!! A query engine for intelligence data needs to support ! various levels of believability. We can support believability in "#!! ! !0123&*1! TT-IQ by using type modality [29]. In other words, we can annotate type with a modality operator that represents a level !! !!!"#$%&'!!"#$%&'(!!"#$$%&' ! !! ! !!"#!!! !! !"#$%!&" !! ! ! !! of believability, such as certain, likely, not!likely, and ! !!!"#$%&! ! !!!"#$%&"'! ! ! !"#$ !! ! ! !!! !! !!! !!!"#$!!! !!! impossible. Then an analyst could prove a hypothesis represented by the type ! is likely to occur as the judgment "#!!! $%&'&()*&+(! ! ⊢ ! !"#$!%! : !"#! or disprove it by proving the judgment ! ⊢ ! !"#$%%!&'(! : !"#!. !! !!!"#$%&'!!"#$%&'(!!"#$$%&'(! ! !"# ! !!! !! !"#$%!&" !! ! ! !! ! !!!"#$%&! ! !!!"#$%&"'! ! ! !"#$ !! ! ! !!! !! !!! !!!"#$ !! ! ! B. Too complex for an analyst The formalism of TT-IQ and the method of reasoning "#!!! employed by TT-IQ may be too complicated for an analyst. We don't expect the analyst to specify queries in the formal !! !!!"#$%&'!!"#$!"#$!!"#$$%&'(! ! !"# ! !! language of TT-IQ, but in natural language similar to that used ! !!!"#$%&! ! !!!"#$%&"'! ! ! !"#$ !! ! ! !!! !! !!! !!!"#$ !! ! ! in Fig. 1. We could employ a technique similar to that used in [14] to allow end users to specify queries using natural language. !! !!!"#$%&'!!"#$%&'(!!"#$$%&'(! ! !"# ! !!! !! !"#$%!&" !! ! ! C. Non-determinism and Subtyping Since a type may have multiple subtypes, a tactic that finds "#!,()%#*&-!$.)%/)*&+(! ! ! !!! ! !!! or creates a subtype of a type could be nondeterministic. In other words, the tactic may not produce the same subtype for the same supertype. As a result, the query engine could !! !!!"#$%&'!!"#$%&'(!!"#$$%&'(! ! !"# ! !!!!"#!! produce different results for the same query over the same data. We can resolve non-determinism by asking the user to select the appropriate subtype. This approach would be similar to !! !!!"#$%&'!!"#$%&'(!!"#$$%&'(! ! !"# ! !!! !!!"#$%!&" !! ! faceted search. The query engine would require the end user to ! !!! !!!"#$%!&"!!! !!! select from a list of subtypes to use as a candidate to narrow the search space. D. Implementation of TT-IQ !"#!!"#$%& !! !!! !!!"#$%!&" !! ! ! !!!! Currently, we are in the planning stage of creating an implementation of TT-IQ. We plan to create an implementation of TT-IQ using Coq and R. Coq will provide the interactive ! ! !"#$%& ! !"#!$%&%!!!"#$%&"' ! !! !! reasoning capability. R will be used as the language and runtime for defining and executing analytics. We anticipate !! !!!"#$%&'!!"#$%&'(!!"#$$%&'(! ! !"# having to add a library to R to provide a more seamless ! !"#$%& ! !"#!$%&%!!!"#$%&"' ! !! !!"#! interaction with RDF than the existing R libraries. We consider this implementation of TT-IQ a proof-of- Fig. 5. Proof tree illustrating ∃ rules and analytic evaluation. concept implementation. We plan to use this implementation to conduct research to address usability issues and determine ![!/!]:prop. strengthens and weaknesses of interactive semantic querying over automatic semantic querying. Recall in Fig. 1, we used the Narrow Concept tactic to replace Attack with IED. Narrow Concept contains code to The analyst workstation will contain an analytic framework select the appropriate concept to use as the subtype for the that would provide an interface to support contribution of Narrow Type rule. After it finds a subtype, it asks the rule analytics written in a wide range of languages, such as engine to apply Narrow Type to a target type judgment in a MATLAB, C, Java, and Python. proof tree. The rule engine creates a new judgment using the antecedent of Narrow Type as a template. The new judgment is VI. CONCLUSION added as a child of the target type judgment. The rule engine In this paper, we showed how to apply techniques from returns the new proof tree to Narrow Concept and Narrow ITPs (interactive theorem provers) to analyze military Concept returns the proof tree to the query engine. Fig. 5 intelligence. Users of ITPs apply small programs called tactics contains a portion of the proof tree created from the Geo in an iterative fashion to construct a proof. We demonstrated Search and Concept Introduction tactics in Fig. 1. how tactics could be used to answer semantic queries interactively. Furthermore, we showed how to incorporate V. DISCUSSION STIDS 2013 Proceedings Page 115 analytics that use machine learning, knowledge discovery, or Velegrakis, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012, network analysis into the querying process. pp. 109–130. [11] S. Ferré, A. Hermann, and M. Ducassé, “Combining Faceted Search A. Future Work and Query Languages for the Semantic Web,” in Advanced Information Systems Engineering Workshops, C. Salinesi and O. Pastor, Eds. In "Believability", we eluded to an approach to handle Springer Berlin Heidelberg, 2011, pp. 554–563. uncertainty. Future work should investigate this approach. [12] H. Pérez-Urbina, E. Rodrıguez-Dıaz, M. Grove, G. Konstantinidis, and Also, we should consider how to incorporate the approach in E. Sirin, “Evaluation of query rewriting approaches for OWL 2,” in Proc. of the Joint Workshop on Scalable and High-Performance [15] into our type system. Semantic Web Systems (SSWS+ HPCSW 2012), 2012, vol. 943. In the future, we would like to investigate how to [13] G. Tecuci, Building intelligent agents: an apprenticeship multistrategy learning theory, methodology, tool and case studies. San Diego: implement interactive querying in an existing military Academic Press, 1998. intelligence cloud system, such as the DCGS-A Cloud. We [14] G. Tecuci, M. Boicu, C. Boicu, D. Marcu, B. Stanescu, and M. believe our approach to querying would be a good fit for the Barbulescu, “The Disciple–Rkf Learning and Reasoning Agent,” semantic enhancement approach adopted by the DCGS-A Computational Intelligence, vol. 21, no. 4, pp. 462–479, 2005. Cloud. [15] M. Boicu, D. Marcu, G. Tecuci, and D. Schum, “Cognitive Assistants for Evidence-Based Reasoning Tasks,” in 2011 AAAI Fall Symposium Series, 2011. ACKNOWLEDGMENT [16] G. Tecuci, D. Schum, M. Boicu, D. Marcu, and Hamilton, Benjamin, Rod Moten thanks Andy Zhao of Sotera Defense Solutions “TIACRITIS System and Textbook: Learning Intelligence Analysis through Practice,” in Proceedings of the Fifth International Conference and Dr. Aaron Stump of the University of Iowa on their on Semantic Technologies for Intelligence, Defense, and Security, 2010. valuable feedback on the ideas expressed in this paper. [17] G. Tecuci, D. Marcu, M. Boicu, D. Schum, and K. Russell, “Computational Theory and Cognitive Assistant for Intelligence REFERENCES Analysis,” in Proceedings of the Sixth International Conference on Semantic Technologies for Intelligence, Defense, and Security – STIDS 2011, Fairfax, VA, USA, 2011, pp. 66–75. [1] Wylie Wong, “The Army Brings the Cloud to the Battlefield,” FedTech [18] S. F. Allen, M. Bickford, R. L. Constable, R. Eaton, C. Kreitz, L. Magazine, 31-Jul-2013. [Online]. Available: Lorigo, and E. Moran, “Innovations in computational type theory using http://www.fedtechmagazine.com/article/2013/07/army-brings-cloud- Nuprl,” Journal of Applied Logic, vol. 4, no. 4, pp. 428–469, Dec. 2006. battlefield. [Accessed: 22-Aug-2013]. [19] Interactive Theorem Proving and Program Development - Coq’Art: The [2] S. Miakhel, “Understanding Afghanistan: The importance of tribal Calculus of Inductive Constructions. . culture and structure in security and governance,” Asian Survey, vol. 35, [20] T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL: A Proof no. 7, 1995. Assistant for Higher-Order Logic. Springer, 2002. [3] B. Ulicny, G. M. Powell, C. J. Matheus, M. Coombs, and M. M. Kokar, [21] R. Dapoigny and P. Barlatier, “Using a Dependently-Typed Language “Priority Intelligence Requirement Answering and Commercial for Expressing Ontologies,” in Knowledge Science, Engineering and Question-Answering: Identifying the Gaps,” DTIC Document, 2010. Management, H. Xiong and W. B. Lee, Eds. Springer Berlin [4] LTG Keith Alexander, BG Mike Ennis, Robert L. Grossman, James Heidelberg, 2011, pp. 257–268. Heath, Russ Richardson, Glenn Tarbox, and Eric Sumner, “Automating [22] R. Dapoigny and P. Barlatier, “Formal foundations for situation Markup of Intelligence Community Data: A Primer,” Defense awareness based on dependent type theory,” Information Fusion, vol. Intelligence Journal, no. 12–2, pp. 83–96, 2003. 14, no. 1, pp. 87–107, Jan. 2013. [5] D. Davis, R. Lichtenwalter, and N. V. Chawla, “Supervised methods [23] G. De Giacomo, M. Lenzerini, and R. Rosati, “Higher-Order for multi-relational link prediction,” Soc. Netw. Anal. Min., vol. 3, no. 2, Description Logics for Domain Metamodeling.,” in Proceedings of the pp. 127–141, Jun. 2013. Twenty-Fifth AAAI Conference on Artificial Intelligence, 2011, pp. 183– [6] D. Davis, R. Lichtenwalter, and N. V. Chawla, “Multi-relational Link 188. Prediction in Heterogeneous Information Networks,” in 2011 [24] F. A. Lisi, “A Declarative Modeling Language for Concept Learning in International Conference on Advances in Social Networks Analysis and Description Logics,” in Inductive Logic Programming, F. Riguzzi and Mining (ASONAM), 2011, pp. 281–288. F. Železný, Eds. Springer Berlin Heidelberg, 2013, pp. 151–165. [7] S. David, M. Tatiana, H. Alan, C. Shaun, and S. Barry, “Integration of [25] Z. Abedjan and F. Naumann, “Improving RDF Data Through Intelligence Data through Semantic Enhancement,” in Proceedings of Association Rule Mining,” Datenbank Spektrum, vol. 13, no. 2, pp. the Sixth International Conference on Semantic Technologies for 111–120, Jul. 2013. Intelligence, Defense, and Security, Fairfax, VA, USA, pp. 6–13. [26] C. Benzmüller and A. Pease, “Higher-order aspects and context in [8] B. Smith, T. Malyuta, W. S. Mandrick, C. Fu, K. Parent, and M. Patel, SUMO,” Web Semantics: Science, Services and Agents on the World “Horizontal Integration of Warfighter Intelligence Data: A Shared Wide Web, vol. 12–13, pp. 104–117, Apr. 2012. Semantic Resource for the Intelligence Community,” in Proceedings of [27] M.-L. Mugnier, “Ontological query answering with existential rules,” the Seventh International Conference on Semantic Technologies for in Proceedings of the 5th international conference on Web reasoning Intelligence, Defense, and Security, 2012. and rule systems, Berlin, Heidelberg, 2011, pp. 2–23. [9] D. Liben-Nowell and J. Kleinberg, “The link-prediction problem for [28] Moten, Rod, “Using a Type-theoretic Approach to Resolve social networks,” Journal of the American society for information Heterogeneity in Data Fusion,” in Proceedings of the National science and technology, vol. 58, no. 7, pp. 1019–1031, 2007. Symposium on Sensor and Data Fusion 2012, Washington, D.C., 2012. [10] G. Zenz, X. Zhou, E. Minack, W. Siberski, and W. Nejdl, “Interactive [29] A. Nanevski, F. Pfenning, and B. Pientka, “Contextual modal type Query Construction for Keyword Search on the Semantic Web,” in theory,” ACM Trans. Comput. Logic, vol. 9, no. 3, pp. 23:1–23:49, Jun. Semantic Search over the Web, R. De Virgilio, F. Guerra, and Y. 2008. STIDS 2013 Proceedings Page 116