I’m working on (1) computer vision for augmented reality [my Phd], (2) machine learning for theorem provers, (3) building the Oxford Transhumanists, and (4) an iPhone app called relaxing stories
1) I build models of the wearer’s environment that include meaningful labels like “floor”, “wall”, “table top”. This will hopefully help us leverage 3D models for figuring out where objects, people, events, and interactions are happening and where they are likely to happen in the future.
2) Should theorem provers use training data? I think so. Theorem proving is provably impossible in general, humans are good at it because we learn to recognise patterns. I’m transforming the ATP problem from an abstract search problem over proofs to a black-box that searches greedily, asking at each point which direction to search next. The problem is then to learn which patterns indicate a fruitful search direction by examining a large corpos of previous proofs.
I’m working on (1) computer vision for augmented reality [my Phd], (2) machine learning for theorem provers, (3) building the Oxford Transhumanists, and (4) an iPhone app called relaxing stories
1) I build models of the wearer’s environment that include meaningful labels like “floor”, “wall”, “table top”. This will hopefully help us leverage 3D models for figuring out where objects, people, events, and interactions are happening and where they are likely to happen in the future.
2) Should theorem provers use training data? I think so. Theorem proving is provably impossible in general, humans are good at it because we learn to recognise patterns. I’m transforming the ATP problem from an abstract search problem over proofs to a black-box that searches greedily, asking at each point which direction to search next. The problem is then to learn which patterns indicate a fruitful search direction by examining a large corpos of previous proofs.
3) http://www.facebook.com/group.php?gid=265828309853
4) http://relaxingstories.com/