\section{Problem Solving}

An important goal of the SCG is to make the 
learners better problem solvers.
The problems to be solved:
Find good claims (true or optimal claims) and 
find good provideInstance and solveInstance functions.

Lab Reductions are a useful tool in this process.
Lab L1 is a reduction of lab L2 if a winning strategy
for L1 implies a winning strategy for L2.

======from slides

With the next example we show the usefulness of lab reductions. A lab L1 reduces to a lab L2 (L1 < L2) if a defense strategy for the claims in L2 guarantees a defense strategy for the claims in L1. Ideally, the claims in L2 are simpler.

L1 reduces to L2 if we can use a black box for L2 to solve L1. The black box makes all perfect decisions, including claims it can defend.

A mapping from L1 to L2 is a computable function f Domain Claim   such that for any 
L1.Domain L2.Domain
L1.Claim L2.Claim 
propose
oppose/agree
provideInstance
solveInstance
refute

=========

Incremental approach
A successful refutation of claim c is viewed as a small step
towards a proof of the negation of c.
If the proponent is perfect, the successful refutation counts as a proof
of !c
because the perfect proponent would have found a way to defend
if such a defense of !c exists.

A successful defense of claim c is viewed as a small step
towards a proof of c.
If the opponent is perfect, the successful defense counts as a proof
of c
because the perfect opponent would have found a way to refute
if such a refutation of c exists.
Restriction: if the opponent is not perfect, it is possible that
c is false and the defense happened because the opponent made a mistake.

