What was the first original proof assistant, what was it used for, when was it created, is it still used today, who created it and what was its' purpose(s)?