View: session overviewtalk overview

09:10 | SPEAKER: Steffen Hölldobler ABSTRACT. We discuss the evaluation of conditionals. Under classical logic a conditional of the form \textit{A implies B} is semantically equivalent to \textit{not A or B}. However, psychological experiments have repeatedly shown that this is not how humans understand and use conditionals. We introduce an innovative abstract reduction system under the three-valued {\L}ukasiewicz logic and the weak completion semantics, that allows us to reason abductively and by revision with respect to conditionals, in three values. We discuss the strategy of \textit{minimal revision followed by abduction} and discuss two notions of relevance. Psychological experiments will need to ascertain if these strategies and notions, or a variant of them, correspond to how humans reason with conditionals. |

09:35 | SPEAKER: Josef Urban ABSTRACT. BliStr is a system that automatically develops strong targetted theorem-proving strategies for the E prover on a large set of diverse problems. The main idea is to interleave (i) iterated low-timelimit local search for new strategies on small sets of similar easy problems with (ii) higher-timelimit evaluation of the new strategies on all problems. The accumulated results of the global higher-timelimit runs are used to define and evolve the notion of "similar easy problems'", and to control the evolution of the next strategy. The technique significantly strengthened the set of E strategies used by the MaLARea, E-MaLeS, and E systems in the CASC@Turing 2012 competition, particularly in the Mizar division. Similar improvement was obtained on the problems created from the Flyspeck corpus. |

10:30 | SPEAKER: Dirk Walther ABSTRACT. We investigate the logical difference problem between general EL-TBoxes. The logical difference is the set of concept subsumptions that are logically entailed by a first TBox but not by a second one. We first reduce the logical difference between two EL-TBoxes to fixpoint reasoning w.r.t. EL-TBoxes. We show how entailments of the first TBox can be represented by subsumptions of least fixpoint concepts by greatest fixpoint concepts which can then be checked w.r.t. the second TBox. The subsumption checks are based on checking for the existence of simulations between hypergraph representations of the fixpoint concept and the TBoxes, not relying on intricate automata-theoretic techniques. |

10:55 | SPEAKER: Eugenia Ternovska ABSTRACT. The paper proposes formal foundations of combined multi-language constraint solving in the form of an algebra of modular systems. The basis for integration of different formalisms is the classic model theory. Each atomic module is a class of structures. It can be given e.g. by a set of constraints in a constraint formalism that has an associated solver. Atomic modules are combined using a small number of algebraic operations. The algebra simultaneously resembles Codd's relational algebra, (but is defined on classes of structures instead of relational tables), and process algebras originated in the work of Milner and Hoare. The data complexity of the basic algebraic operations does not add more than non-deterministic polynomial time to the complexity of atomic modules, which implies, at least theoretically, solvability of modular systems using individual modules as oracles. Finally, we discuss modular system containment and possible notions of equivalence for our algebra. |

11:20 | SPEAKER: Veronika Thost ABSTRACT. Ontology-based query answering augments classical query answering in databases by adopting the open-world assumption and by including domain knowledge provided by an ontology. We investigate temporal query answering w.r.t. ontologies formulated in DL-Lite, a family of description logics that captures the conceptual features of relational databases and was tailored for efficient query answering. We consider a recently proposed temporal query language that combines conjunctive queries with the operators of propositional linear temporal logic (LTL). In particular, we consider negation in the ontology and query language, and study both data and combined complexity of query entailment. |

11:45 | Multiclassifier System with Dynamic Model of Classifier Competence Applied to the Control of Bioprosthetic Hand SPEAKER: Marek Kurzynski ABSTRACT. In this paper the problem of recognition of patient's intent to move hand prosthesis is addressed. The proposed method is based on recognition of electromiographic (EMG) and mechanomiographic (MMG) biosignals using a multiclassifier system (MCS) working with dynamic ensemble selection (DES) scheme and original concept of competence function. The competence measure is based on relating the response of the classifier with the decision profile of a test object which is evaluated using K nearest objects from the validation set (static mode). Additionally, feedback information coming from bioprosthesis sensors on the correct/incorrect classification is applied to the adjustment of the combining mechanism during MCS operation through adaptive tuning competences of base classifiers depending on their decisions (dynamic mode). Experimental investigations using real data concerning the recognition of five types of grasping movements and computer-simulated procedure of generating feedback signals are performed. The performance of MCS with proposed competence measure is experimentally compared against 4 state-of-art MCS's in static mode and furthermore the MCS system developed is evaluated with respect to the effectiveness of the procedure of tuning competence. The results obtained indicate that modification of competence of base classifiers during the working phase essentially improves performance of the MCS system. The system developed achieved the highest classification accuracy demonstrating the potential of MCS with feedback signals from prosthesis sensors for the control of bioprosthetic hand. |

13:40 | SPEAKER: Mats Carlsson ABSTRACT. Some constraint programming solvers and constraint modelling languages feature the SORT(L,P,S) constraint, which holds if S is a nondecreasing rearrangement of the list L, the permutation being made explicit by the optional list P. However, such sortedness constraints do not seem to be used much in practice. We argue that reasons for this neglect are that it is impossible to require the underlying sort to be stable, so that SORT cannot be guaranteed to be a total-function constraint, and that L cannot contain tuples of variables, some of which form the key for the sort. To overcome these limitations, we introduce the StableKeysort constraint, decompose it using existing constraints, and propose a propagator. This new constraint enables a powerful modelling idiom, which we illustrate by elegant and scalable models of two problems that are otherwise hard to encode as constraint programs. |

14:05 | SPEAKER: Maria Andreina Francisco ABSTRACT. Automata allow many constraints on sequences of variables to be specified in a high-level way for constraint programming solvers. An automaton with accumulators induces a decomposition of the specified constraint into a conjunction of constraints with existing inference algorithms, called propagators. Towards improving propagation, we design a fully automated tool that selects, in an off-line process, constraints that are implied by such a decomposition. We show that a suitable problem-specific choice among the tool-selected implied constraints can considerably improve solving time and propagation, both on a decomposition in isolation and on entire constraint problems containing the decomposition. |

14:30 | SPEAKER: Michael Bukatin ABSTRACT. We consider two classes of computations which admit taking linear combinations of execution runs: probabilistic sampling and generalized animation. We argue that the task of program learning should be more tractable for these architectures than for conventional deterministic programs. We look at the recent advances in the ``sampling the samplers" paradigm in higher-order probabilistic programming. We also discuss connections between partial inconsistency, non-monotonic inference, and vector semantics. |

14:55 | SPEAKER: Gvanca Tsulaia ABSTRACT. The article proposes a multi-attribute decision making (MADM) approach, which is applied to the problem of optimal selection of the investment projects. This novel methodology comprises two stages. First, it makes ranking of projects based on TOPSIS (Technique for Order Preference by Similarity to Ideal Solution) method presented in hesitant fuzzy environment. We consider the case when the information on the weights of the attributes is completely unknown. The identification of the weights of the attributes is made in the context of hesitant fuzzy sets and is based on the De Luca-Termini information entropy. The ranking of alternatives is made in accordance with the proximity of their distance to the positive and negative ideal solutions. Second stage of the methodology allows making the most profitable investment in several projects simultaneously. The decision on an optimal distribution of allocated investments among the selected projects is provided using the method developed by the authors for a possibilistic bicriteria optimization problem. An investment example is given to illustrate the application of the proposed approach. |