The AKRRIV project will develop the necessary tools and frameworks to facilitate interoperability between ARIVA systems at the visual level. During AKRRIV three systems will be designed and implemented: Vivid-CL, a logic which handles visual information; RASCALS^IA, a framework for building models of intelligence analysts, including goals, plans, and beliefs; and Director, a system to manage the interaction between systems. Slate will be the first system enhanced with these new developments.

While current Q&A systems are competent and useful with respect to the information they process, they are very limited when compared to a conversation an analyst could have with a human who has read the same information. Solomon, a radically new Q&A system that will transcend the limitations of existing systems by approaching real conversation with real humans.

Solomon is capable of producing rational, justified answers for conceptual, hypothetical, and even open-ended questions related to knowledge bases derived from reading documents. The theoretical approach underlying the system - which, in short, is to model Q&A on a more sophisticated form of human-machine interaction: one in which the machine has the power of cutting-edge machine reasoning technology.

Psychometric AI is the field devoted to building information processing entities capable of at least solid performance on all established, validated tests of intelligence and mental ability - a class of tests that includes IQ tests, tests of reasoning, of creativity, mechanical ability, and so on.

PERI, a robot capable of perfect performance on the Block Design subtest of the Wechsler Adult Intelligent Scale, is our first step towards satisfying this goal.

Can you ascertain if a human or machine has learned a domain solely by direct inspection of the brain, rather than testing for performance? This question is the driving idea behind our Poised-For Learning project, which seeks to concretely engineer a computational system that will learn by reading content as it appears to humans, something no previous system has been able to do. Since textual content read by humans is often supplemented with diagrams and pictures, we are also developing the system to have the ability to reason over diagrammatic and visual content.

Athena, developed by Kostas Arkoudas, a research professor at RPI, is a programming language and an interactive theorem proving environment that integrates computation and deduction. As a programming language, Athena is a higher-order dynamically typed functional programming language with side effects, similar to Scheme. As a logic tool, Athena is a proof checker for a novel formulation of Fitch-style natural deduction for first-order logic with equality, sorts, and polymorphism; and an interactive theorem proving system for discovering theorems. It incorporates facilities for high-performance automated theorem proving and for model generation. It has a rich and fluid language for writing tactics for proof search, and supports inductive reasoning over arbitrary first-order datatypes.

Slate is a multi-faceted intelligent assistant to those whose jobs (and whose training) are in large part reasoning-based. The primary audience is the intelligence community: intelligence analysts, and those studying the art and science of intelligence analysis. Slate is also an assistant to other professional reasoners (e.g., logicians), and students of these other professions. The bulk of the support that has allowed development to this (v3 is about to be released) has come from ARDA, with contributions from DARPA as well. Slate has many distinguishing characteristics that make it quite unique, including:

• Methods and an interface that supports rendering arguments, proofs, scenarios, counterexamples, etc. in visual form.
• Powered by new forms of visual reasoning that exceed standard linguistic/textual reasoning in standard logics (like first-order logic).
• Seamless integration with all the fastest standard provers in the world today (e.g., Vampire, Otter, Oscar, etc.), and with the best model finder as well.
• Automatic generation of first drafts of English reports to then be polished by the human user.
• Built-in libraries of case studies and problems.
• Support for all established forms of reasoning: deduction, induction, abduction (particularly the Wigmorean variety), probabilistic -- all of these available in a visual form.
• New, effective forms of hypothesis generation.
• CL/IKL-compatible for interoperability with existing and future databases, knowledge bases, and other IA tools and technologies.

For more information, see the various presentations and demonstrations of Slate on this site.

Advanced synthetic characters don't merely evoke *beliefs* that they have various mental properties; rather, they must actually *have* such properties. You might (e.g.) believe a standard synthetic character to be evil, but you would of course be wrong. An *advanced* synthetic character, however, can literally *be* evil, because it has the requisite desires, beliefs, and cognitive powers. Our approach is based on the new RASCALS cognitive architecture, which uses simple logical systems (first-order ones) for low-level (perception & action) and mid-level cognition, and advanced logical systems (e.g., epistemic and deontic logics) for more abstract cognition.

Wargaming has a long and distinguished history, dating from H.G. Wells' Little Wars to today's strategy and action games in the entertainment field, and to high-stakes planning in advance of actual battle.

However, all these games are marked by at least two severe limitations:

• One, the humans represented in them are anything but human-level. Real humans have ethical and religious beliefs, have histories, can communicate in languages, and so on. (Our first advanced synthetic character is known simply as 'E.')
• Two, whereas actions taken in real war have consequences that reach to the psychological, social, political, ... spheres, in current wargames everything pivots around simple kinetic consequences.

Our R&D is devoted to building wargames that feature advanced synthetic characters having the cognitive capacities of real humans, whether friend or foe; and to ones in which all spheres of human existence are simulated.

To this end, with support from AFOSR, and previous support from AFRL, we are currently implementing a system (PsyPre) with predictive capability, to, first, make predictions about agents playing our enhanced version of a psychologically rich wargame called `Nicaragua!', and at games abstracted from Nicaragua!. This game shows how modern revolutionary warfare works, and involves both military and political struggles, in addition to such decisive factors as intelligence operations and propaganda. A snapshot from the game is shown at left.

Consider a binary alphabet Turing Machine which is given an infinite, blank tape as input. If this machine halts, we define its productivity as the number of 1's left on the tape after the machine is run to completion. If it does not halt, the machine is given a productivity value of zero. Now consider all of the binary alphabet Turing Machines that have n states. The machine in this set which has the highest productivity is called a Busy Beaver, and its productivity is the result of the Busy Beaver function BB(n).

Existential Graphs is a graphical logic system developed by C.S. Peirce in 1909. He had found the linear notation and accompanying rules of traditional logic systems involved and unintuitive, so he created a system that allowed the user to express logical statements in a completely graphical way.

Our project is an effort to develop an interactive interface for using the Existential Graphs system and to explore automated theorem proving and automated proof generation utilizing the system.

The objective of the Grid Logic project is to create formal systems of "grid logic" applicable to various grid-based logic puzzles. We hope to create a general-purpose grid logic engine and interface into which the user can stick different puzzle modules for specific puzzle environments.

By then applying the various grid logic rules, the user would not only be able to solve the puzzle, but at the same time create a proof for the correctness and uniqueness of that solution as well. Also, a proof checker can indicate if and where the user made an invalid inference. Our hope is to use this environment as a more engaging environment to teach students basic principles of logic.