I just had an interesting chat with Daniel where he brought up a feature he would like to see in ProofPeer.
Basically, what he would like is that you can write up a math test in ProofPeer which students can then solve. After some discussion, we agreed that on an abstract level this would mean having a feature, where you are not only asking if an x with a certain logical property Phi(x) exists (or uniquely exists), but also to require x to fulfil a meta property M(x) which is defined on the term representation of such an x. Obviously this could be extended to more than one variable.
As an example, it would be nice if you could for example pose the following question in ProofPeer:
Find x and y such that Phi(x, y) holds and M(x, y) is fulfilled, where
I just had an interesting chat with Daniel where he brought up a feature he would like to see in ProofPeer.
Basically, what he would like is that you can write up a math test in ProofPeer which students can then solve. After some discussion, we agreed that on an abstract level this would mean having a feature, where you are not only asking if an x with a certain logical property Phi(x) exists (or uniquely exists), but also to require x to fulfil a meta property M(x) which is defined on the term representation of such an x. Obviously this could be extended to more than one variable.
As an example, it would be nice if you could for example pose the following question in ProofPeer: Find x and y such that Phi(x, y) holds and M(x, y) is fulfilled, where