Report on Ahmed Abdelmeged's Progress During the Summer Semester 2013

During the Summer semester, Ahmed has passed the Comprehensive Exam and has made substantial progress towards completing his dissertation. http://www.ccs.neu.edu/home/mohsen/thesis-ahmed/thesis-ahmed.pdf gives the current version.

His progress has been disseminated in three talks at two Swiss Universities (ETH Zurich and University of Applied Sciences Rapperswil) and ABB Research:

http://www.ccs.neu.edu/home/lieber/talks/summer-2013/eth/
http://www.ccs.neu.edu/home/lieber/talks/summer-2013/rapperswil/
http://www.ccs.neu.edu/home/lieber/talks/summer-2013/abb/
All three talks had the same title: Software Development with Semantic Games. The talks were useful in collecting feedback from several communities and were well received.

Ahmed's dissertation experimentally determines a good algorithm called SCG-Competition to select the best Skolem functions (a.k.a. avatars) for defending interpreted logical statements. The defending is based on semantic games associated with the interpreted logical statements. SCG-Competition engages the avatars in a tournament (using well-known tournament mechanisms TMs) which use position selection mechanisms (PSMs). PSMs are a new generalization of semantic games needed for SCG-Competition. SCG-Competition ranks the avatars based on their performance in the tournament and chooses the best avatar which contains the "best" Skolem functions.

A set of TMs and PSMs have been determined and experiments with avatars with predetermined skill levels are being prepared to find an optimal selection of TM and PSM. The experiments will be completed in 3 weeks.

The thesis of the dissertation is: Semantic games of interpreted logic statements provide a useful foundation to collectively, with several unreliable scholars, solve the computational problems implied by the semantic games.

The progress made includes a simplified model. Instead of doing claim evaluation seperately, it is now done as a side effect of avatar evaluation. This simplification eliminates one dimension of the complexity of algorithm SCG-Competition. It simplifies the experimental evaluation.

The work to be done includes (1) the experimental selection of the best components for SCG-Competition (2) completing a few more labs in the formal science wikipedia (fswikipedia.net is not yet live) (3) writing the dissertation which currently has 56 pages (see link above).

I am confident that Ahmed can complete this work this fall semester. Indeed, the plan is that he will give the dissertation to the committee in September. My earlier prediction that he would complete this summer turned out to be wrong. One reason was that the model was too complex but now it has been simplified.

The committee has given significant help to Ahmed complementing my skills. Thomas and others proposed dropping crowdsourcing from the title and using it only as an application, Yizhou proposed the use of avatars with predetermined skill levels and Thomas and Christo and Casper have given feedback on a draft in mid summer which Ahmed and I have been taking very seriously. This feedback has helped me improve my 3 presentations.

Let me reiterate that the applications of Ahmed's work are significant: software development, making formal sciences more accessible, to education in formal sciences.