Transcript PersistentPlaygrounds

Persistent Playgrounds
Fall 2011
Managing Software Development
3/27/2016
Persistent Playgrounds
1
Alternative Introduction
• From an Independence-Friendly Logic website.
3/27/2016
Persistent Playgrounds
2
Quantifier Game of Lovers
• http://mtl.uta.fi/logic-group/iflogic.html
• Bob and Alice are two lovers who can never seem to
agree about anything. Whenever Alice makes a claim,
Bob immediately tries to refute it. If Alice makes an
existential claim, Bob demands that she identify an
individual satisfying it. When Alice asserts a negated
formula the lovers switch roles: Bob attempts to
defend the claim, whilst Alice tries to refute it.
• When Alice asserts an ordinary first-order claim, the
ensuing dispute is a game of perfect information. If the
claim is true, Alice will always win. If it is false, Bob will
always win.
3/27/2016
Persistent Playgrounds
3
Proofs / Winning Strategies
• Skolemization is the process of eliminating the
existential quantifiers from a formula by
introducing fresh function symbols.
• A Skolem function produces a witness for an
existential claim. Taken together, a set of Skolem
functions for a claim can be seen as encoding a
strategy for Alice in the associated semantic
game. If the claim is true, the Skolem functions
can be assumed to encode a winning strategy.
3/27/2016
Persistent Playgrounds
4
Persistent Playgrounds
Persistent Playground
• Tracks the evolution of
solution techniques in a
domain over several years.
• Compares old approaches with
new ones. The new
approaches should succeed
over all old ones.
• Builds incrementally a
knowledge base through a
sequence of tournaments.
Develops the techniques to
defend the claims in
knowledge base.
3/27/2016
Isolated Playground
• Persistent playground with
only one tournament.
Persistent Playgrounds
5
Comparison
Persistent Playground
• tournament
• second opinion evaluation
• data mining
– strongly defended
3/27/2016
Isolated Playground
• tournament
• nothing
• data mining
– two agree
Persistent Playgrounds
6
Second Opinion
• After a tournament is complete we have:
– welfare set from previous tournament
– strongly defended claims -> might be true
– strongly refuted claims -> might be false
• Apply data mining step.
• Many of the strongly defended or refuted claims
have not been seen by many avatars.
• All avatars must give their decision (refute,
strengthen or agree) on each strongly defended
or refuted claim as well as on the old welfare
claims.
3/27/2016
Persistent Playgrounds
7
Second Opinion
• The second opinion evaluation will change the
set of strongly defended and refuted claims.
• The second opinion evaluation is like a
tournament but without proposing claims.
Instead claims come from data mining.
• Apply data mining step again.
3/27/2016
Persistent Playgrounds
8
SCG
• Tournament
– list of claims with statistics
• Datamining Results of Tournament
– WelfareClaims
• strongly defended claims
– DemocraticCleanup
• claims are even more strongly defended or they are less
strongly defended and dropped from the welfare set.
All vote with justification.
3/27/2016
Persistent Playgrounds
9
Statistics collected for claim
• list of proposers
• for each claim and proposer
– how often defended
• reputation of defender at time of defense
– how often refuted
• reputation of refuters at time of refutation
3/27/2016
Persistent Playgrounds
10
Statistics collected for claim
• for each claim
– how often defended
• average reputation of defender at time of defense
– how often refuted
• average reputation of refuters at time of refutation
3/27/2016
Persistent Playgrounds
11
Data mining: welfare claims
simple
•
•
•
•
C : d: defended r: refuted
d: how often defended
r: how often refuted
Keep it simple
– d/(d+r) > 0.99: true welfare claims
– r/(d+r) > 0.99: false welfare claims
3/27/2016
Persistent Playgrounds
12
Data mining: welfare claims
more complex
•
•
•
•
C : d: defended (ard) r: refuted (arr)
d: how often defended
r: how often refuted
More complex:
– d*ard/(d*ard+r*arr) > 0.99: true welfare claims
– r*arr/(d*ard+r*arr) > 0.99: false welfare claims
• ard: average reputation of defender
• arr: average reputation of refuter
3/27/2016
Persistent Playgrounds
13
Why reputation
• if r1>r2:
– claim C is defended against an opposer with
reputation r1 counts more than
– claim C is defended against an opposer with
reputation r2
3/27/2016
Persistent Playgrounds
14
Events
• refute
– defender
• current reputation
– opposer
• current reputation
– claim
– outcome: refuted/defended
3/27/2016
Persistent Playgrounds
15
Events
• strengthen
– reduces to refute and the strengthened claim has
Bob as defender
– if strengthening not successful we have a
successful defense of the original claim
•
•
•
•
3/27/2016
defender
opposer
claim
defended
Persistent Playgrounds
16
Events
• agree
– reduces to refute and Bob becomes also a
proposer of the claim
3/27/2016
Persistent Playgrounds
17
Old
3/27/2016
Persistent Playgrounds
18
Why reputation
• if r1>r2:
– claim C is defended by a proposer with against an
opposer with reputation r1 counts more than
– claim C is defended against an opposer with
reputation r2
– difference reputation(proposer)reputation(opposer)
3/27/2016
Persistent Playgrounds
19
Comparison
New
• tournament
• second opinion evaluation
• data mining
– strongly defended
3/27/2016
Old
• tournament
• nothing
• data mining
– two agree
Persistent Playgrounds
20
Playground Comparisons
HSR
MMG
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
•
Kind: ForAllExists
Instance: (n,k)
InstanceSet: singleton
Solution: decision tree
quality: depth of tree
solve: minimize
claim: HSR(n,k)<=q
strengthen: yes, smaller q.
skills needed: Pascal’s triangle,
memoization
3/27/2016
ForAllExists
x
[0,1]
y
f(x,y)=xy+(1-x)(1-y2)
maximize
k(c): AxEy f(x,y)>=c
yes, larger c.
skills: calculus, exploring a
surface
Persistent Playgrounds
21