ABSTRACT. Many search problems, from artificial intelligence to combinatorics, explore large search spaces to determine the presence or absence of a certain object. These problems are hard due to combinatorial explosion, and have traditionally been called infeasible. The brute-force method, which at least implicitly explores all possibilities, is a general approach to search systematically through such spaces. Brute force has long been regarded as suitable only for simple problems. This has changed in the last two decades, due to the progress in satisfiability (SAT) solving, which renders brute force into a powerful approach to deal with many problems easily and automatically. We illustrate the strength of SAT via the Boolean Pythagorean Triples problem, which has been a long-standing open problem in Ramsey Theory. Our parallel SAT solver allowed us to solve the problem on a cluster in about two days using 800 cores, demonstrating its linear time speedup on many hard problems. Due to the general interest in this mathematical problem, our result requires a formal proof. Exploiting recent progress in unsatisfiability proof checking, we produced and verified a clausal proof of the smallest counterexample, which is almost 200 terabytes in size. These techniques show great promise for attacking a variety of challenging problems arising in mathematics and computer science.

ABSTRACT. We extend the terminological formalism of the well-known description logic ALC from concept inclusions (CIs) to more general constraints formulated in the quantifier-free fragment of Boolean Algebra with Presburger Arithmetic (QFBAPA). In QFBAPA one can formulate Boolean combinations of inclusion constraints and numerical constraints on the cardinalities of sets. Our new formalism extends, on the one hand, so-called cardinality restrictions on concepts, which have been introduced two decades ago, and on the other hand the recently introduced statistical knowledge bases. Though considerably more expressive, our formalism has the same complexity (NExpTime) as cardinality restrictions on concepts. We will also introduce a restricted version of our formalism for which the complexity is ExpTime. This yields the until now unknown exact complexity of the consistency problem for statistical knowledge bases.

ABSTRACT. In this paper we study Secrecy-Preserving Query Answering problem under the OpenWorld Assumption (OWA) for Prob-EL>0;=1 Knowledge Bases (KBs). We have designed a tableau procedure to compute a semi model M over the given KB which eventually is equivalent to a probabilistic model to KB. Given a secrecy set S, which is a finite set of assertions, we compute a function E, called an envelope of S, which assigns a set E() of assertions to each world in the semi modal M. E provides logical protection to the secrecy set S against the reasoning of a querying agent. Once the semi model M and an envelope E are computed, we define the secrecy-preserving semi model ME. Based on the information available in ME, assertional queries with probabilistic operators can be answered eciently while preserving secrecy. To the best of our knowledge, this work is first one studying secrecy-preserving reasoning in description logic augmented with probabilistic operators. When the querying agent asks a query q, the reasoner answers “Yes” if information about q is available in ME; otherwise, the reasoner answers “Unknown”. Being able to answer “Unknown” plays a key role in protecting secrecy under OWA. Since we are not computing all the consequences of the knowledge base, answers to the queries based on just secrecy-preserving semi model ME could be erroneous. To fix this problem, we further augment our algorithms by providing recursive query decomposition algorithm to make the query answering procedure foolproof. 1

ABSTRACT. Incorporating a dynamic kick engine that is both fast and effective is pivotal to be competitive in one of the world’s biggest AI and robotics initiatives: RoboCup. Using the NAO robot as a testbed, we developed a dynamic kick engine that can generate a kick trajectory with an arbitrary direction without prior input or knowledge of the parameters of the kick. The trajectories are generated using cubic splines (two degree three polynomials with a via-point), cubic Hermite splines or sextics (one six degree polynomial). The trajectories are executed while the robot is dynamically balancing on one foot. Although a variety of kick engines have been implemented by others, there are only a few papers that demonstrate how kick engine parameters have been optimized to give an effective kick or even a kick that minimizes energy consumption and time. Parameters such as kick configuration, limits of the robot, or shape of the polynomial can be optimized. We propose an optimization framework based on the Webots simulator to optimize these parameters. Experiments on different joint interpolators for kick motions have been observed to compare results.

ABSTRACT. We describe the multi-agent-based 3-dimensional (3D) interactive training system (IVT) for early career teachers (ECT) in high poverty schools, to practice their skills in managing disruptive students behaviors with diverse 3D virtual student avatars in 3D virtual classrooms (see Figure 1). Our aims are to address some limitations of existing training systems for teachers [1]: (1) our virtual students are autonomous agents rather than existing virtual students controlled by a human using Wizard of Oz human-computer interaction method; (2) IVT is the first training system for training educators that uses state of the art webGL graphics to enable browser-independent unlimited system accessibility (versus existing that are PC-based); (3) our 3D WebGL graphics and animations are very realistic and can be rendered seamlessly in real- time on any browser; (4) the number of virtual students populating our virtual classrooms is significantly higher than other systems (i.e. we have 15 virtual students vs. 5 students in existing systems) in order to increase the believability of the system and users sense of immersion in the virtual classrooms; (5) we built dialogue-based interactions for ECT users and student avatars; (6) we ensured high system usability and enhanced user experience (UX); and (7) we integrated high-quality childrens stereo voice recordings within the students autonomous behaviors. To develop IVT, we programed simulated autonomous students behavior derived from the content of 12 large vignettes developed by our team education experts. We adapted Hartson’s and Pyla’s [2] human-centered methodology to build IVT along three iterative parallel software design and development lifecycles: a 3D graphics lifecycle, an interaction design lifecycle, and a software engineering lifecycle including the use of a multi-agent system for modeling virtual agent behaviors [3].

ABSTRACT. We propose using abduction for inferring implicit rules for Smart City ontologies. We show how we can use Z3 to extract candidate abducers from partial ontologies and leverage them in an iterative process of evolving an ontology by refining relations and restrictions, and populating relations.

Our starting point is a Smart City initiative of the city of Barcelona, where a substantial ontology is being developed to support processes such as city planning, social services, or improving the quality of the data concerning (for instance) legal entities, whose incompleteness may sometimes hide fraudulent behavior. In our scenario we are supporting semantic queries over heterogeneous and noisy data. The approach we develop would allow evolving ontologies in an iterative fashion as new relations and restrictions are discovered.

ABSTRACT. Poster by D. Dormagen, I. Makarenko

Project of Computational Metaphysics lecture course (by C. Benzmüller, A. Steen and M. Wisniewski) at FU Berlin in 2016.

ABSTRACT. Poster by M. Bentert, Y. Lewash, D. Streit, S. Stugk

Project of Computational Metaphysics lecture course (by C. Benzmüller, A. Steen and M. Wisniewski) at FU Berlin in 2016.

ABSTRACT. Research on iterated belief change has focussed mostly on belief revision, only few papers have addressed iterated belief contraction. Most prominently, Darwiche and Pearl published seminal work on iterated belief revision the leading paradigm of which is the so-called principle of conditional preservation. In this paper, we use this principle in a thoroughly axiomatized form to develop iterated belief contraction operators for Spohn's ranking functions. We show that it allows for setting up constructive approaches to tackling the problem of how to contract a ranking function by a proposition or a conditional, respectively, and that semantic principles can also be derived from it for the purely qualitative case.

ABSTRACT. Maximum entropy reasoning (ME-reasoning) based on relational conditionals combines both the capability of ME-distributions to express uncertain knowledge in a way that excellently fits to commonsense, and the great expressivity of an underlying first-order logic. The drawbacks of this approach are its high complexity which is generally paired with a costly domain size dependency, and its non-transparency due to the non-existent a priori independence assumptions as against in Bayesian networks. In this paper we present some independence results for ME-reasoning based on the aggregating semantics for relational conditionals that help to disentangle the composition of ME-distributions, and therefore, lead to a problem reduction and provide structural insights into ME-reasoning.

ABSTRACT. Herbrand structures are a subclass of standard first-order structures that carry significant definitional content. This paper is devoted to the logics induced by them: Herbrand and semi-Herbrand logics, with and without equality. The rich expressiveness of these logics entails that there is no adequate effective proof system for them. We therefore introduce infinitary proof systems for Herbrand logics, and prove their completeness. Natural and sound finitary approximations of the infinitary systems are also presented.