8 Mar
2011
8 Mar
'11
12:21 p.m.
On Mar 8, 8:20 pm, Tom Hawkins
I am curious -- how easy is it to use theoremquest for playing with equational theories?
Let me turn the question around: How easy is it to play with equational theories in HOL Light? Because this is the planed basis for TheoremQuest.
Dunno... I am far from being a theorem-prover buff/expert :-) I know of Dijkstra-Scholten logic -- not as a formal logician but as a math teacher. But anyhow that (HOL) gives me some context and sense of direction -- Thanks.