GCAI 2016:Papers with AbstractsPapers 

Abstract. Nonclassical logics (such as modal logics, description logics, conditional logics, multivalued logics, hybrid logics, etc.) have many applications in artificial intelligence. In this tutorial, we will demonstrate a generic approach to automate propositional and quantified variants of nonclassical logics using theorem proving systems for classical higherorder logic. Our particular focus will be on quantified multimodal logics. We will present and discuss a semantical embedding of quantified multimodal logics into classical higherorder logic, which enables the encoding and automated analysis of nontrivial modal logic problems in the Isabelle/HOL proof assistant. Additionally, TPTP compliant automated theorem proving systems can be called from within Isabelle’s Sledgehammer tool for automating reasoning tasks. In the tutorial, we will apply this approach to exemplarily solve a prominent puzzle from the AI literature: the wellknown wise men.  Abstract. In automated reasoning it is common that firstorder formulas need to be translated into clausal normal form for proof search. The structure of this normal form can have a large impact on the performance of firstorder theorem provers, influencing whether a proof can be found and how quickly. It is common folklore that transformations should ideally minimise both the size of the generated clause set and extensions to the signature. This paper introduces a new topdown approach to clausal form generation for firstorder formulas that aims to achieve this goal in a new way. The main advantage of this approach over existing bottomup techniques is that more contextual information is available at points where decisions such as subformulanaming and Skolemisation occur. Experimental results show that our implementation of the transformation in Vampire can lead to clausal forms which are smaller and better suited to proof search.  Abstract. Stateoftheart SAT solvers are highly tuned systematicsearch procedures augmented with formula simplification techniques. They emit unsatisfiability proofs in the DRAT format to guarantee correctness of their answers. However, the DRAT format is inadequate to model some parallel SAT solvers such as the awardwinning system \plingeling. In \plingeling, each solver in the portfolio applies clause addition and elimination techniques. Clause sharing is restricted to clauses that do not contain melted literals. In this paper, we develop a transition system that models the computation of such parallel portfolio solvers. The transition system allows us to formally reason about portfolio solvers, and we show that the formalism is sound and complete. Based on the formalism, we derive a new proof format, called parallel DRAT, which can be used to certify UNSAT answers.  Abstract. This paper introduces a new technique for reasoning with quantifiers and theories. Traditionally, firstorder theorem provers (ATPs) are well suited to reasoning with firstorder problems containing many quantifiers and satisfiability modulo theories (SMT) solvers are well suited to reasoning with firstorder problems in ground theories such as arithmetic. A recent development in firstorder theorem proving has been the AVATAR architecture which uses a SAT solver to guide proof search based on a propositional abstraction of the firstorder clause space. The approach turns a single proof search into a sequence of proof searches on (much) smaller subproblems. This work extends the AVATAR approach to use a SMT solver in place of the SAT solver, with the effect that the firstorder solver only needs to consider groundtheoryconsistent subproblems. The new architecture has been implemented using the Vampire theorem prover and Z3 SMT solver. Our experimental results, and the results of recent competitions, show that such a combination can be highly effective.  Abstract. Automated theorem provers for firstorder logic usually operate on sets of firstorder clauses. It is wellknown that the translation of a formula in full firstorder logic to a clausal normal form (CNF) can crucially affect performance of a theorem prover. In our recent work we introduced a modification of firstorder logic extended by the first class boolean sort and syntactical constructs that mirror features of programming languages. We called this logic FOOL. Formulas in FOOL can be translated to ordinary firstorder formulas and checked by firstorder theorem provers. While this translation is straightforward, it does not result in a CNF that can be efficiently handled by stateoftheart theorem provers which use superposition calculus. In this paper we present a new CNF translation algorithm for FOOL that is friendly and efficient for superpositionbased firstorder provers. We implemented the algorithm in the Vampire theorem prover and evaluated it on a large number of problems coming from formalisation of mathematics and program analysis. Our experimental results show an increase of performance of the prover with our CNF translation compared to the naive translation.  Abstract. Inspired by recent work in machine translation and object detection, we introduce an attentionbased model that automatically learns to extract information from an image by adaptively assigning its capacity across different portions of the input data and only processing the selected regions of different sizes at high resolution. This is achieved by combining two modules: an attention subnetwork which uses a mechanism to model a humanlike counting process and a capacity subnetwork. This subnetwork efficiently identifies input regions for which the attention model output is most sensitive and to which we should devote more capacity and dynamically adapt the size of the region. We focus our evaluation on the Cluttered MNIST, SVHN, and Cluttered GTSRB image datasets. Our findings indicate that the proposed model is able to drastically reduce the number of computations, compared with traditional convolutional neural networks, while maintaining similar or better performance.  Abstract. We study the problem of learning the importance of preferences in preference profiles in two important cases: when individual preferences are aggregated by the ranked Pareto rule, and when they are aggregated by positional scoring rules. For the ranked Pareto rule, we provide a polynomialtime algorithm that finds a ranking of preferences such that the ranked profile correctly decides all the examples, whenever such a ranking exists. We also show that the problem to learn a ranking maximizing the number of correctly decided examples (also under the ranked Pareto rule) is NPhard. We obtain similar results for the case of weighted profiles when positional scoring rules are used for aggregation.  Abstract. With the rapid progress of network technologies and multimedia data, information retrieval techniques gradually become contentbased, and not textbased yet. In this paper, we propose a contentbased image retrieval system to query similar images in a real image database. First, we employ segmentation and main object detection to separate the main object from an image. Then, we extract MPEG7 features from the object and select relevant features using the SAHS algorithm. Next, two approaches “oneagainst all” and “oneagainstone” are proposed to build the classifiers based on SVM. To further reduce indexing complexity, Kmeans clustering is used to generate MPEG7 signatures. Thus, we combine the classes predicted by the classifiers and the results based on the MPEG7 signatures, and find out the similar images to a query image. Finally, the experimental results show that our method is feasible in image searching from the real image database and more effective than the other methods.  Abstract. This paper deals with the problem of scheduling prioritized patient in emergency department laboratories according to a triage factor. The problem is considered as a flexible open shop scheduling problem with the objective of minimizing the total completion time of prioritized patients. In this research, patient scheduling is addressed with a harmony search algorithm with wheelroulette selection technique. Then, a comparative study is performed by considering results of genetic algorithm. Simulations on real data from emergency department show that the proposed approach improves significantly the total completion time of patients especially those with severe conditions.  Abstract. This paper tackles the automatic matching of job seekers and recruiters, based on the logs of a recruitment agency (CVs, job announcements and application clicks). Preliminary experiments reveal that good recommendation performances in collaborative filtering mode (emitting recommendations for a known recruiter using the click history) coexist with poor performances in cold start mode (emitting recommendations based on the job announcement only). A tentative interpretation for these results is proposed, claiming that job seekers and recruiters $$ whose mother tongue is French $$ yet do not speak the same language. As first contribution, this paper shows that the information inferred from their interactions differs from the information contained in the CVs and job announcements. The second contribution is the hybrid system \XX (MAtching JObs and REsumes), where a deep neural net is trained to match the collaborative filtering representation properties. The experimental validation demonstrates \XX merits, with good matching performances in cold start mode.  Abstract. Surgery lighting systems (SLS) aim to provide optimal lighting conditions for the surgeon in an operating room. To visually differentiate between only marginally different looking tissues, SLS offer settings for the level of illumination, color temperature and size of the illuminated field. By today’s standards, SLS are controlled with control panels that are situated at the lamp housings. The operation of the control panel is handled in an ergonomically unfavorable position with the hands above the operator’s head. On top, the region above the operator’s shoulder is considered as not sterile and causes a potential safety risk. To secure asepsis, it is required to extensively sterilize all equipment that the operator comes in contact with. In this paper, a contactless gesture control for a SLS is developed with the intention to offer the surgeon a sterile and ergonomically comfortable operation. A Microsoft Kinect 3Dsensor is used. The gesture control offers control of the level of illumination, the color temperature and functions of a camera for documentation requirements like zooming, rotating and taking a picture. A sophisticated procedure to logon and logoff the system prevents unintentional operation. The gesture control system and the conventional control panel were tested and compared in a usability study. The participating subjects rated the usability of the gesture control to be good to very good according to the System Usability Scale by Broke. 94% of the subjects perceived the gesture control to be ergonomically more comfortable. After simultaneous operation of the surgery light and execution of a cognitive task, 82% stated that the gesture control is less likely to distract them from that task. This data indicates that the concept of a gesture control with a 3Dsensor for a SLS is feasible and that it has a potential to receive a high degree of acceptance.  Abstract. We show how the problem of deciding the existence of uniform interpolants of TBoxes formulated in the Description Logic \EL can be divided into three subproblems based on a characterisation of the logical difference between \ELTBoxes. We propose a prooftheoretic decision procedure for subsumer interpolants of general TBoxes formulated in the Description Logic \EL, solving one of these subproblems. A subsumer interpolant of a TBox depends on a signature and on a concept name. It is a TBox formulated using symbols from the signature only such that, both, it follows from the original TBox and it exactly entails the subsumers formulated in the signature that follow from the concept name \wrt~the original TBox. Our decision procedure first constructs a graph that exactly represents the part of original TBox that is describable using signature symbols only. Subsequently, it is checked whether a graphrepresentation of the original TBox can be simulated by the constructed graph, in which case a subsumer interpolant exists. We also evaluate our procedure by applying a prototype implementation on several biomedical ontologies.  Abstract. Certain approaches for missingdata imputation propose the use of learning techniques to identify regularities and relations between attributes, which are subsequently used to impute some of the missing data. Prior theoretical results suggest that the soundness and completeness of such learningbased techniques can be improved by applying rules anew on the imputed data, as long as one is careful in choosing which rules to apply at each stage. This work presents an empirical investigation of three natural learningbased imputation policies: training rules once and applying them repeatedly; training new rules at each iteration; continuing the training of previous rules at each iteration. We examine how the three policies fare across different settings. In line with the predictions of the theory, we find that an iterative learnpredict approach is preferable.  Abstract. According to psychological models, learned knowledge can be distinguished into implicit and explicit knowledge. The former can be exploited, but cannot be verbalized easily (e.\,g., to explain it to another person). The latter is available in an explicit form, it often comprises generalized, rulebased knowledge which can be verbalized and explained to others. During a learning process, the learned knowledge starts in an implicit form and gets explicit as the learning process progresses, and humans benefit from exploiting such generalized, rulebased knowledge when learning. This paper investigates how learning agents can benefit from explicit knowledge which is extracted during a learning process from a learned implicit representation. It is clearly shown that an agent can already benefit from explicit knowledge in early phases of a learning process.  Abstract. Humans have the impressive capability to efficiently find nearoptimal solutions to complex, multistep problems. AI planning can model such problems well, but is inefficient for realistic problems. We propose to use AI planning in combination with a shortterm memory, inspired by models of human shortterm memory, to structure realworld problem domains and make the planning process more efficient, while still producing satisficing solutions. We evaluate the method in the domain of a household robot.  Abstract. Robot navigation in domestic environments is still a challenge. This paper introduces a cognitively inspired decisionmaking method and an instantiation of it for (local) robot navigation in spatially constrained environments. We compare the method to two existing local planners with respect to efficiency, safety and legibility.  Abstract. This paper addresses the modeling and design of Systems of Systems (SoS) as well as inter multiagent systems cooperation. It presents and illustrates a new generic model to describe formally SoS. Then, this model is used to propose a study of interAMAS (Adaptive MultiAgent System) cooperation. Each AMAS, reified as a componentsystem of a SoS, uses a cooperative decision process in order to interact with other AMAS and to collectively give rise to a relevant overall function at the SoS level. The proposed model as well as the interAMAS study are instantiated to a simulated resources transportation problem.  Abstract. Identification of implicit structures in dynamic systems is a fundamental problem in Artificial Intelligence. In this paper, we focus on General Game Playing where games are modeled as finite state machines. We define a new property of game states called invariant projections which strongly corresponds to humans' intuition of game boards and may be applied in General Game Playing to support powerful heuristics, and to automate the design of game visualizations. We prove that the computation of invariant projections is Pi_{2}^{P}complete in the size of the game description. We also show that invariant projections form a lattice, and the lattice ordering may be used to reduce the time to compute invariant projections potentially by a factor that is exponential in the schema size of game states. To enable competitive general game players to efficiently identify boards, we propose a sound (but incomplete) heuristic for computing invariant projections and evaluate its performance.  Abstract. The exploitation of solar power for energy supply is of increasing importance. While technical development mainly takes place in the engineering disciplines, computer science offers adequate techniques for optimization. This work addresses the problem of finding an optimal heliostat field arrangement for a solar tower power plant. We propose a solution to this global, nonconvex optimization problem by using an evolutionary algorithm. We show that the convergence rate of a conventional evolutionary algorithm is too slow, such that modifications of the recombination and mutation need to be tailored to the problem. This is achieved with a new genotype representation of the individuals. Experimental results show the applicability of our approach.  Abstract. Computational psychology provides computational models exploring different aspects of cognition. A cognitive architecture includes the basic aspects of any cognitive agent. It consists of different correlated modules. In general, cognitive architectures provide the needed layouts for building intelligent agents. The paper presents the a rulebased approach to visually animate the simulations of models done through cognitive architectures. As a proof of concept, simulations through Adaptive Control of ThoughtRational (ACTR) were animated. ACTR is a wellknown cognitive architecture. It was deployed to create models in different fields including, among others, learning, problem solving and languages.  Abstract. Local Compatibility Matrices (LCMs) are mechanisms for computing heuristics for graph matching that are particularly suited for matching qualitative constraint networks enabling the transfer of qualitative spatial knowledge between qualitative reasoning systems or agents. A system of LCMs can be used during matching to compute a premove evaluation, which acts as a prior optimistic estimate of the value of matching a pair of nodes, and a postmove evaluation which adjusts the prior estimate in the direction of the true value upon completing the move. We present a metaheuristic method that uses reinforcement learning to improve the prior estimates based on the posterior evaluation. The learned values implicitly identify unprofitable regions of the search space. We also present data structures that allow a more compact implementation, limiting the space and time complexity of our algorithm.  Abstract. Constraint Programming is a powerful and expressive framework for modelling and solving combinatorial problems. It is nevertheless not always easy to use, which has led to the development of highlevel specification languages. We show that Constraint Logic Programming can be used as a metalanguage to describe itself more compactly at a higher level of abstraction. This can produce problem descriptions of comparable size to those in existing specification languages, via techniques similar to those used in data compression. An advantage over existing specification languages is that, for a problem whose specification requires the solution of an auxiliary problem, a single specification can unify the two problems. Moreover, using a symbolic representation of domain values leads to a natural way of modelling channelling constraints.  Abstract. This paper introduces Deep Incremental Boosting, a new technique derived from AdaBoost, specifically adapted to work with Deep Learning methods, that reduces the required training time and improves generalisation. We draw inspiration from Transfer of Learning approaches to reduce the startup time to training each incremental Ensemble member. We show a set of experiments that outlines some preliminary results on some common Deep Learning datasets and discuss the potential improvements Deep Incremental Boosting brings to traditional Ensemble methods in Deep Learning.  Abstract. \noindent The growing neural gas (GNG) algorithm is an unsupervised learning method that is able to approximate the structure of its input space with a network of prototypes. Each prototype represents a local input space region and neighboring prototypes in the GNG network correspond to neighboring regions in input space. Here we address two problems that can arise when using the GNG algorithm. First, the GNG network structure becomes less and less meaningful with increasing dimensionality of the input space as typical distance measures like the Euclidean distance loose their expressiveness in higher dimensions. Second, the GNG itself does not provide a form of output that retains the discovered neighborhood relations when compared with common distance measures. We show that a GNG augmented with {\em local input space histograms} can mitigate both of these problems. We define a sparse vector representation as output of the augmented GNG that preserves important neighborhood relations while pruning erroneous relations that were introduced due to effects of high dimensionality.  Abstract. \tit{Partial lexicographic preference trees}, or \tit{PLPtrees}, form an intuitive formalism for compact representation of qualitative preferences over combinatorial domains. We show that PLPtrees can be used to accurately model preferences arising in practical situations, and that highaccuracy PLPtrees can be effectively learned. We also propose and study learning methods for a variant of our model based on the concept of a PLPforest, a collection of PLPtrees, where the preference order specified by a PLPforest is obtained by aggregating the orders of its constituent PLPtrees. Our results demonstrate the potential of both approaches, with learning PLPforests showing particularly promising behavior.  Abstract. Sentiment analysis refers to the use of natural language processing to identify and extract subjective information from textual resources. One approach for sentiment extraction is using a sentiment lexicon. A sentiment lexicon is a set of words associated with the sentiment orientation that they express. In this paper, we describe the process of generating a general purpose sentiment lexicon for Persian. A new graphbased method is introduced for seed selection and expansion based on an ontology. Sentiment lexicon generation is then mapped to a document classification problem. We used the Knearest neighbors and nearest centroid methods for classification. These classifiers have been evaluated based on a set of hand labeled synsets. The final sentiment lexicon has been generated by the best classifier. The results show an acceptable performance in terms of accuracy and Fmeasure in the generated sentiment lexicon.  Abstract. Natural Language Understanding (NLU) has been a longstanding goal of AI and many related fields, but it is often dismissed as very hard to solve. NLU is required complex flexible systems that take action without further human intervention. This inherently involves strong semantic (meaning) capabilities to parse queries and commands correctly and with high confidence, because an error by a robot or automated vehicle could be disastrous. We describe an implemented general framework, the ECG2 system, that supports the deployment of NLU systems over a wide range of application domains. The framework is based on decades of research on embodied actionoriented semantics and efficient computational realization of a deep semantic analyzer (parser). This makes it linguistically much more flexible, general and reliable than existing shallow approaches that process language without considering its deeper semantics. In this paper we describe our work from a Computer Science perspective of system integration, and show why our particular architecture requires considerably less effort to connect the system to new applications compared to other language processing tools. 

