The agents must constructively demonstrate what they claim.
They must interact 
with the acceptors of their challenges and convince them
that their constructive proof is correct.
For example, if an agent (called Alice)
 claims that she has a prrof for the statement:

Exists f in F For All J in FS(f) prop(f,J),

Alice must be prepared to deliver an f in F so that Bob,
the acceptor of her challenge, cannot find a J so that !prop(f,J).
If Bob succeeds to negate the predicate prop, Alice's proof 
is not credible. The J that Bob finds is polynomial in 
the size of f.
The predicate prop(f,J) must be computable in polynomial time.

Alice and Bob engage in a dialog to prove that 
Alice' proof is not credible. 

This is similar in spirit to interactive proof systems
where a prover and verifier interact until the verifier
is convinced that the proof is correct.
In SCG Alice and Bob interact with the goal that Alice 
convinces Bob that her proof is credible.
Both Alice and Bob live in a resource-bounded environment.

Situations:
Bob is convinced that Alice is credible
Alice is not credible

If Alice is perfect and Alice is not credible => !Fact
If Alice and Bob are perfect and Bob is convinced that Alice is credible => Fact

Credible interactive proofs
(or error-finding interaction)
are weaker than interactive proofs.
Credible interactive proofs are about finding holes in the
reasoning of the other agents and not necessarily
in finding a proof.
It is important that the holes can be easily checked.

There is a weak connection to program checking,
also a topic in interactive proofs.
http://www.cs.princeton.edu/theory/complexity/ipchap.pdf
8.7 Program Checking


Credible interactive proofs are defined for claims 
with an even number of alternating quantifiers.

======================

http://plato.stanford.edu/entries/mathematics-constructive/

Constructive Mathematics
First published Tue Nov 18, 1997; substantive revision Thu May 21, 2009
Constructive mathematics is distinguished from its traditional counterpart, classical mathematics, by the strict interpretation of the phrase .there exists. as .we can construct.. In order to work constructively, we need to re-interpret not only the existential quantifier but all the logical connectives and quantifiers as instructions on how to construct a proof of the statement involving these logical expressions. 

Although certain individuals . most notably Kronecker . had expressed disapproval of the .idealistic., nonconstructive methods used by some of their nineteenth century contemporaries, it is in the polemical writings of L.E.J. Brouwer (1881.1966), beginning with his Amsterdam doctoral thesis (Brouwer 1907) and continuing over the next forty-seven years, that the foundations of a precise, systematic approach to constructive mathematics were laid. In Brouwer's philosophy, known as intuitionism, mathematics is a free creation of the human mind, and an object exists if and only if it can be (mentally) constructed.

SEARCH for Specker in the above document !!!

.Specker, E., 1949, .Nicht konstruktiv beweisbare Säe der Analysis., J. Symbolic Logic, 14: 145.158.


===================================
Interesting question:

which algorithms correspond to constructive proofs
of facts of the form EAEA ... prop?

-----------
We find errors in constructive proofs.

What about secret challenges.
claim: for all inputs f in F, my alg. will 

claim: there is a formula f in F, where your algorithm 
will not come within p of my secret for f.

e f in F: prop

claim: there is a formula f in F, where your algorithm 
will not reconstruct my secret for f or a solution
of the same or better quality.
variant:

Duel:
We both have submitted our algorithms:
claim: if you give me 10 problems
and I give you 10 problems 
(simultaneously) my algorithm will solve
your problems better than your algorithm will solve my problems.

kinds of challenges:
I believe that I can constructively support the
following claim. If you accept the challenge,
you must prove my belief wrong using an example.

challenges:
mathematical
secret
duel

SCG is about proving constructive beliefs wrong constructively
by engaging in a protocol whose outcome contradicts the belief.


What is a constructive belief:

I believe I can construct an object f in F
for which you cannot find an object J(f): !prop(f,J).

I believe I can construct an object f in F
for which I know a secret solution s
that you cannot find in time t(f).

I believe I can construct k problems in F
and you cannot construct k problems in F
so that your algorithm has worse performance on my k 
problems than mine on your k problems.


Also has flavor of finding an error in a proof