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.
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.
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.
Currently there is a representation theorem that shows that the ranking must be fault based.
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?
How can complex claims be decomposed into simpler claims. Introduce problem reductions. See proposal.
The dissertation focuses on algorithm competitions. But the approach is broader. It can be used to settle claims in any formal science.
Which claims are true but don't have a recursive = algorithmic winning strategy?
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.
What has Independence-Friendly logic to offer? There exist indeterminate claims without a winning strategy.
We started with our own protocol language. Is this useful for social sciences where refutations are not formal?
How can interpreted claims be used in this context? How is the data best embedded in a structure?
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/
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.
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?
Can we use automated techniques to show that S is not winning and can be improved?