Interactive multi-objective particle swarm optimisation using decision space interaction

The most common approach to decision making in multi-objective optimisation with metaheuristics is a posteriori preference articulation. Increased model complexity and a gradual increase of optimisation problems with three or more objectives have revived an interest in progressively interactive decision making, where a human decision maker interacts with the algorithm at regular intervals. This paper presents an interactive approach to multi-objective particle swarm optimisation (MOPSO) using a novel technique to preference articulation based on decision space interaction and visual preference articulation. The approach is tested on a 2D aerofoil design case study and comparisons are drawn to non-interactive MOPSO. © 2013 IEEE.

Fast Rule Mining over Multi-dimensional Windows

Association rule mining is an indispensable tool for discovering
insights from large databases and data warehouses.
The data in a warehouse being multi-dimensional, it is often
useful to mine rules over subsets of data defined by selections
over the dimensions. Such interactive rule mining
over multi-dimensional query windows is difficult since rule
mining is computationally expensive. Current methods using
pre-computation of frequent itemsets require counting
of some itemsets by revisiting the transaction database at
query time, which is very expensive. We develop a method
(RMW) that identifies the minimal set of itemsets to compute
and store for each cell, so that rule mining over any
query window may be performed without going back to the
transaction database. We give formal proofs that the set of
itemsets chosen by RMW is sufficient to answer any query
and also prove that it is the optimal set to be computed
for 1 dimensional queries. We demonstrate through an extensive
empirical evaluation that RMW achieves extremely
fast query response time compared to existing methods, with
only moderate overhead in pre-computation and storage

An Interactive Theorem Prover for First-Order Dynamic Logic

Dynamic logic is an extension of modal logic originally intended for reasoning about computer programs. The method of proving correctness of properties of a computer program using the well-known Hoare Logic can be implemented by utilizing the robustness of dynamic logic. For a very broad range of languages and applications in program veri cation, a theorem prover named KIV (Karlsruhe Interactive Veri er) Theorem Prover has already been developed. But a high degree of automation and its complexity make it di cult to use it for educational purposes. My research work is motivated towards the design and implementation of a similar interactive theorem prover with educational use as its main design criteria. As the key purpose of this system is to serve as an educational tool, it is a self-explanatory system that explains every step of creating a derivation, i.e., proving a theorem. This deductive system is implemented in the platform-independent programming language Java. In addition, a very popular combination of a lexical analyzer generator, JFlex, and the parser generator BYacc/J for parsing formulas and programs has been used.

Multi-objective image segmentation with an interactive evolutionary computation approach

In this paper, a multi-objective image segmentation approach with an Interactive Evolutionary Computation (IEC)-based framework is presented. Two objectives, i.e., the overall deviation and the connectivity measure, are optimized simultaneously using a mu

Interactive theorem provers: issues faced as a user and tackled as a developer

Interactive theorem provers (ITP for short) are tools whose final aim is to certify proofs written by human beings. To reach that objective they have to fill the gap between the high level language used by humans for communicating and reasoning about mathematics and the lower level language that a machine is able to “understand” and process. The user perceives this gap in terms of missing features or inefficiencies. The developer tries to accommodate the user requests without increasing the already high complexity of these applications. We believe that satisfactory solutions can only come from a strong synergy between users and developers. We devoted most part of our PHD designing and developing the Matita interactive theorem prover. The software was born in the computer science department of the University of Bologna as the result of composing together all the technologies developed by the HELM team (to which we belong) for the MoWGLI project. The MoWGLI project aimed at giving accessibility through the web to the libraries of formalised mathematics of various interactive theorem provers, taking Coq as the main test case. The motivations for giving life to a new ITP are: • study the architecture of these tools, with the aim of understanding the source of their complexity • exploit such a knowledge to experiment new solutions that, for backward compatibility reasons, would be hard (if not impossible) to test on a widely used system like Coq. Matita is based on the Curry-Howard isomorphism, adopting the Calculus of Inductive Constructions (CIC) as its logical foundation. Proof objects are thus, at some extent, compatible with the ones produced with the Coq ITP, that is itself able to import and process the ones generated using Matita. Although the systems have a lot in common, they share no code at all, and even most of the algorithmic solutions are different. The thesis is composed of two parts where we respectively describe our experience as a user and a developer of interactive provers. In particular, the first part is based on two different formalisation experiences: • our internship in the Mathematical Components team (INRIA), that is formalising the finite group theory required to attack the Feit Thompson Theorem. To tackle this result, giving an effective classification of finite groups of odd order, the team adopts the SSReflect Coq extension, developed by Georges Gonthier for the proof of the four colours theorem. • our collaboration at the D.A.M.A. Project, whose goal is the formalisation of abstract measure theory in Matita leading to a constructive proof of Lebesgue’s Dominated Convergence Theorem. The most notable issues we faced, analysed in this part of the thesis, are the following: the difficulties arising when using “black box” automation in large formalisations; the impossibility for a user (especially a newcomer) to master the context of a library of already formalised results; the uncomfortable big step execution of proof commands historically adopted in ITPs; the difficult encoding of mathematical structures with a notion of inheritance in a type theory without subtyping like CIC. In the second part of the manuscript many of these issues will be analysed with the looking glasses of an ITP developer, describing the solutions we adopted in the implementation of Matita to solve these problems: integrated searching facilities to assist the user in handling large libraries of formalised results; a small step execution semantic for proof commands; a flexible implementation of coercive subtyping allowing multiple inheritance with shared substructures; automatic tactics, integrated with the searching facilities, that generates proof commands (and not only proof objects, usually kept hidden to the user) one of which specifically designed to be user driven.

An online e-Learning authoring tool to create interactive multi-device learning objects using e-Infrastructure resources

Education can take advantage of e-Infrastructures to provide teachers with new opportunities to increase students' motivation and engagement while they learn. Nevertheless, teachers need to find, integrate and customize the resources provided by e-Infrastructures in an easy way. This paper presents ViSH Editor, an innovative web-based e-Learning authoring tool that aims to allow teachers to create new learning objects using e-Infrastructure resources. These new learning objects are called Virtual Excursions and are created as reusable, granular and interoperable learning objects. This way they can be reused to build new ones and they can be integrated in websites or Learning Management Systems. Details about the design, development and the tool itself are explained in this paper as well as the concept, structure and metadata of the new learning objects. Lastly, some real examples of how to enrich learning using Virtual Excursions are exposed.

Facilitating the creation of interactive multi-device Learning Objects using an online authoring tool

Learning Objects facilitate reuse leading to cost and time savings as well as to the enhancement of the quality of educational resources. However, teachers find it difficult to create or to find high quality Learning Objects, and the ones they find need to be customized. Teachers can overcome this problem using suitable authoring systems that enable them to create high quality Learning Objects with little effort. This paper presents an open source online e-Learning authoring tool called ViSH Editor together with four novel interactive Learning Objects that can be created with it: Flashcards, Virtual Tours, Enriched Videos and Interactive Presentations. All these Learning Objects are created as web applications, which can be accessed via mobile devices. Besides, they can be exported to SCORM including their metadata in IEEE LOM format. All of them are described in the paper including an example of each. This approach for creating Learning Objects was validated through two evaluations: a survey among authors and a formal quality evaluation of 209 Learning Objects created with the tool. The results show that ViSH Editor facilitates educators the creation of high quality Learning Objects.