The project was funded by EPSRC "First Grant" scheme, between 01 March 2012 and 28 February 2014. It has now officially ended, and below is the project page as it evolved during the two years of the grant duration. This page is no longer updated. However, this grant gave rise to three longer-term research trends; and each of them now has its own webpage, and each is very much alive, healthy, and growing:
The ML-CAP project was about finding statistically significant patterns in computer proofs, and using these patterns to aid proof automation. The Coalgebraic Logic Programming was first used to develop the techniques, but later we switched to working with Coq.
The work split into two lines of research -- marked by 1*. and 2*. below.For ML4PG web-page, see here;
Together with Jonathan Heras, we are working on integration of statistical Machine-learning application into Proof General - a generic interface for interactive theorem provers. We call the result ML4PG: Machine Learning for Proof General. The tool provides users with various proof-hints during the process of proof development. ML4PG now has it own web-page, where you can find software, related documentation, and installation instructions. Follow this link.CoALP is a dialect of first-order Horn-Clause logic that features lazy guarded corecursion and parallelism. CoALP arose from Coalgebraic Semantics for logic programming we developed with John Power between 2008-2012.
In 2012, we were joined by Martin Schmidt, who has helped to implement CoALP first in PROLOG, and then in Parallel language Go. CoALP now has its own mini-page, from which you can view all related publications, slides, and download the prototypes.
Classification Problem 1. ListNat. Data set. Target.
Classification Problem 1. Stream. Data set. Target.
Classification Problem 2.1. ListNat. Data set. Target.
Classification Problem 2.1. ListNat - Extended data set. Data set. Target.
Classification Problem 2.1. Stream. Data Set. Target.
Classification Problem 2.2. Stream. Data Set. Target.
Classification Problem 3. ListNat. Data set. Target.
Classification Problem 3. ListNat - Extended data set. Data set. Target.
Classification Problem 4. Stream. Data Set. Target.
Classification Problem 5. ListNat Data set. Target.
Classification Problem 5. Stream Data set. Target.
------------------------------
Classification Problem 1. Initial Training on ListNat, switching to Stream.
New training set Stream and its target.
Test on a new Stream data set and it's target.
New training set and its target.
Test on a new Stream data set and it's target.
Another test on a new Stream data set and it's target.
Classification Problem 1. Initial Training on Stream, switching to ListNat.
New training set Stream and its target.
Test on a new Stream data set and it's target.
New training set and its target.
Test on a new Stream data set and it's target.
Classification Problem 5. Initial Training on ListNat, switching to Stream.
New training set Stream and its target.
Test on a new Stream data set and it's target.
New training set and its target.
Test on a new Stream data set and it's target.
Classification Problem 5. Initial Training on Stream, switching to ListNat
New training set ListNat and its target.
Test on a new List data set and it's target.
New training set and its target.
Test on a new ListNat data set and it's target.