#
1af7dc8b |
|
16-Sep-2011 |
Ramana Kumar <ramana.kumar@gmail.com> |
better match intended semantics of OpenTheory names rather than using strings, now have a type abbreviation otname for string list * string. it might be worth writing more operations on this type (like for manipulating the namespace).
|
#
c50e432c |
|
10-Sep-2011 |
Ramana Kumar <ramana.kumar@gmail.com> |
functions from thy_{const,tyop} to string in OpenTheoryCommon
|
#
39b041ae |
|
09-Sep-2011 |
Ramana Kumar <ramana.kumar@gmail.com> |
translation to and from opentheory type variable names
|
#
ca80b7e9 |
|
04-Sep-2011 |
Ramana Kumar <ramana.kumar@gmail.com> |
Implement 10 more inference rules on OpenTheory kernel Also rewrite MP, because previous code was likely to loop. 20 rules to go.
|
#
9ee3cfa0 |
|
03-Sep-2011 |
Ramana Kumar <ramana.kumar@gmail.com> |
start work on log_thm Contrary to the initial plan of having an intermediate extended article file format, it seems feasible to do the compilation to the OpenTheory virtual machine on the fly. Being outside of the kernel (and thus in the scope of boolTheory, Drule, etc.) makes this possible. However, we must be careful to avoid implementing an inference rule in terms of itself (and thus sending log_thm into a loop). SUBST is the first rule to pose a challenge (and probably won't be the last), so I've left it for now. Next step is probably to get rid of TODO_prf (by adding proof cases for the remaining rules in Thm).
|
#
60eb85e0 |
|
03-Sep-2011 |
Ramana Kumar <ramana.kumar@gmail.com> |
logging facility work in progress (terms, but not yet theorems)
|