Questions Generated by Ahmed Abdelmeged's Dissertation

  1. Wikipedia for Formal Sciences

    How would a Wikipedia for Formal Sciences be organized? We have labs and lab relations to describe the claims of the specific formal science in refutable form.

  2. Application to Artifact Submission in Formal Sciences

    There is a trend in conference organization, to ask authors to submit an artifact that supports the claim they make in their paper. We propose that authors submit a winning strategy for a claim. Then a full round-robin tournament will determine who has the best artifact. Most likely, the authors will influence the claim formulation but the conference will make the final choice.

  3. Application to calls for proposals.

    A call for proposals is a lab description. Preliminary strategies are submitted (correponding to the proposals) and evaluated using SCG. Then the best performers are invited to submit their final strategies.

  4. Axiomatize the notion of a structured ranking function for side-choosing games.
  5. What is the set of axioms that characterizes ranking based on fault-counting?

    Currently there is a representation theorem that shows that the ranking must be fault based.

  6. Finding a reliable signal in a noisy environment

    The events happening in a tournament can be very noisy. True claims may be refuted and false claims may be defended. We don't know whether a claim is true or not. We want to find the most meritorious player. Is there a statistical counterpart to the axiomatic approach? For ranking in tournaments of regular games both axiomatic and statistical approaches have been studied. Should this be done for side-choosing games as well?

  7. Lab relations

    How can complex claims be decomposed into simpler claims. Introduce problem reductions. See proposal.

  8. How general is the approach?

    The dissertation focuses on algorithm competitions. But the approach is broader. It can be used to settle claims in any formal science.

  9. How serious is the restriction of a recursive winning strategy?

    Which claims are true but don't have a recursive = algorithmic winning strategy?

  10. Simplified Semantic Games.

    This simplifies the writing of strategies. We need a function only for each quantifier. What are the advantages/disadvantages of this approach? Ahmed also allows a vector of values to be given for each quantifier. How does this affect thoroughness.

  11. Other logics supporting semantic games.

    What has Independence-Friendly logic to offer? There exist indeterminate claims without a winning strategy.

  12. Refutation protocols not coming from logics.

    We started with our own protocol language. Is this useful for social sciences where refutations are not formal?

  13. Sciences with claims based on data, e.g., Biological sciences.

    How can interpreted claims be used in this context? How is the data best embedded in a structure?

  14. Information leakage through semantic games.

    If we hide the values there is less feedback and learning. Sometimes the information leakage reveals the general strategy. A well chosen example suggests a proof (see paper by Janos Makowsky, Technion). http://www.cs.technion.ac.il/~janos/

  15. Investigate application to teaching.

    Good Lab design. Divide students into triples (at least one fairly strong) for full round-robin games within each triple. Force randomly.

    Do a controlled experiment in an algorithms class by dividing students into two sets. One learns the traditional way, the other uses SCG to brainstorm and to test their solutions through semantic games.

    Which group performs better in tests?

    Make clear whether faults will be counted or not. Good to have practice games that don't count.

  16. What is the connection between direct proofs and semantic games?

    Three way correspondence: 1. interpreted logical formula F in some structure A (defines software requirements). 2. winning strategy S for semantic game associated with F (expressed as a collection of Skolem functions). Because S is winning, F holds in A. S is the software satisfying the requirements. 3. Constructive proof in some proof system that F holds in A.

    Do you know techniques to translate a proof from 3. into a set of Skolem functions that provide a winning strategy. In other words, how do you get the program from the proof?

  17. Side-choosing games are defined for a combinatorial base game. How to generalize the definition to chance games, such as Poker. Suggested by Andreas Krause.
  18. Are automated techniques such as SMT applicable to the following problem: Given are two items: 1. interpreted logical formula F in some structure A (defines software requirements). 2. winning strategy S for semantic game associated with F (expressed as a collection of Skolem functions). Because S is winning, F holds in A. S is the software satisfying the requirements.

    Can we use automated techniques to show that S is not winning and can be improved?