=Paper=
{{Paper
|id=Vol-1097/STIDS2013_T15
|storemode=property
|title=Analyzing Military Intelligence Using Interactive Semantic Queries
|pdfUrl=https://ceur-ws.org/Vol-1097/STIDS2013_T15_Moten.pdf
|volume=Vol-1097
|dblpUrl=https://dblp.org/rec/conf/stids/Moten13
}}
==Analyzing Military Intelligence Using Interactive Semantic Queries==
https://ceur-ws.org/Vol-1097/STIDS2013_T15_Moten.pdf
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