Publications
By twelve02Drag-and-drop of Formulæ from a Browser
Formulæ in a semantic source such as OpenMath can be presented in web-browsers with the benefit of features that can help in reading and understanding them. Important aspects include the rendering quality as well as tooltips to indicate the semantics of presented symbols. Within the ActiveMath learning environment we have added another feature: the ability to drag-and-drop terms from presented formulæ into formula-input places such as the exercise formula editor, the function
plotter, or to the external world.
This drag-and-drop is initiated using a contextual-menu which comes up by clicking on a presented term. We describe the user-interface limitations that have lead us to require these extra interactions instead of relying on the simple copy-and-paste paradigm. We explain how the current mechanism works and sketch how ActiveMath could collaborate with external receiving applications.
Towards the Verification of the Civitas Remote Electronic Voting Protocol Using ProVerif
The recently proposed Civitas protocol is the first electronic voting system that claims to satisfy formal definitions of crucial properties, such as soundness, individual verifiability, as well as coercion resistance. Particularly the latter is important, since Civitas has been developed as a remote voting system and coercion resistance implies further privacy-type properties, such as vote-privacy and receipt-freeness.
Recent research came up with a new formalization of coercion-resistance in terms of observational equivalence, which can be used for automatic verification and captures simulation and forced-abstention attacks. In this paper we formally study the protocol underlying the Civitas system (Civitas protocol), which we specify in the applied pi-calculus and verify its security properties, namely soundness and coercion resistance, using ProVerif, a resolution-based theorem prover for cryptographic protocols. To our knowledge, we are conducting the first automated analysis of this protocol for an unbounded number of honest and corrupted voters.
Latent Semantic Algorithms for Improving Search Results in an Intelligent Tutoring Environment for Mathematics
The mere mass of electronic information we face nowadays raises a high claim on information retrieval (IR) techniques which, from a users point of view, shall be coevally responsive and easy to use. Whilst, in terms of the World Wide Web and the search for textual and, increasingly, binary content, search engines such as Google or Yahoo! became multi-billion-Dollar businesses, some information remains hardly detectable.
Particularily when working with an interactive E-Learning environment for mathematical education, the learner needs a handy way for querying mathematical contents. In the context of semantic IR in mathematical databases, the explicit annotation of semantic knowledge and approaches based on latent semantic algorithms provide semantic background for the queried information.
This article proposes a method of amending the search engine of an existing Intelligent Tutoring System, ActiveMath, using latent semantic algorithms. This overcomes the drawbacks of explicitly annoted semantic information, metadata, which has to be produced during the creation process of a content item. The aim of this work is to significantly improve the search engine’s precision and recall rates and to find out what field of knowledge the learner most likely points at without relying on explicitly denoted semantics. For this purpose an existing software package for LSA, SemanticVectors, has been integrated into the search facility of the learning environment and, subsequently, the results have been evaluated.
Re-use and Management of Change in Collaborative Authoring
My Master’s topic. Presentation of an evolutionary process of content pieces for the Intelligent Tutoring System ActiveMath, whose quality improves with the number of re-uses. The planned environment supports collaborative development of Learning Objects.