ABSTRACT. In automated reasoning it is common that first-order 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 first-order theorem provers, influencing whether a proof can be found and how quickly. It is common folklore that translations should ideally minimise both the size of the generated clause set and extensions to the signature. This paper introduces a new top-down approach to clausal form generation for first-order formulas that aims to achieve this goal in a new way. The main advantage of this approach over existing bottom-up techniques is that more contextual information is available at points where decisions such as subformula-naming and skolemisation occur. Experimental results show that our implementation of the translation in Vampire can lead to clausal forms which are smaller and better suited to proof search.

ABSTRACT. Contemporary sequential SAT solvers construct certificates in the DRAT format to increase the confidence of their answers for unsatisfiable instances. However, the DRAT format is inadequate to model parallel SAT solvers, such as plingeling, that are based on the portfolio approach with restricted clause sharing and inprocessing. In this paper, we develop a formal model of parallel portfolio solvers that cooperate by restricted clause sharing and apply all known formula simplification techniques. We show that the formalism is sound, complete, and models the computation performed by the award-winning system plingeling. Moreover, we present a new proof format, PDRAT, that can be used to certify UNSAT answers from such portfolio solvers.

ABSTRACT. This paper introduces a new technique for reasoning with quantifiers and theories. Traditionally, first-order theorem provers (ATPs) are well suited to reasoning with first-order problems containing many quantifiers and satisfiability modulo theories (SMT) solvers are well suited to reasoning with first-order problems in ground theories such as arithmetic. A recent development in first-order theorem proving has been the AVATAR architecture which uses a SAT solver to guide proof search based on a propositional abstraction of the first-order clause space. The approach turns a single proof search into a sequence of proof searches on (much) smaller sub-problems. This work extends the AVATAR approach to use a SMT solver in place of the SAT solver, with the effect that the first-order solver only needs to consider ground-theory-consistent sub-problems. 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. Inspired by recent work in machine translation and object detection, we introduce an attention-based 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 sub-network which uses a mechanism to model a human-like counting process and a capacity sub-network. This sub-network 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 polynomial-time 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 NP-hard. 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 content-based, and not text-based yet. In this paper, we propose a content-based 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 MPEG-7 features from the object and select relevant features using the SAHS algorithm. Next, two approaches “one-against-all” and “one-against-one” are proposed to build the classifiers based on SVM. To further reduce indexing complexity, K-means clustering is used to generate MPEG-7 signatures. Thus, we combine the classes predicted by the classifiers and the results based on the MPEG-7 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 wheel-roulette 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 applications clicks). Preliminary experiments reveal that good recommendation performances in collaborative filtering mode (emitting recommendations for a known recruiter using the clicks) co-exist 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 Majore, where a deep neural net is trained to match the collaborative filtering representation properties. The experimental validation demonstrates Majore 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. 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 3D-sensor 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 3D-sensor for a SLS is feasible and that it has a potential to receive a high degree of acceptance.