3 Jun
2011
3 Jun
'11
11:08 a.m.
Am 03.06.2011 10:32, schrieb Guy:
What might --| mean, if not a comment? It doesn't seem possible to define it as an operator. Obviously, anyone who is going to write a formal logic framework would want to define the following operators ;) :
T |- phi: T proves phi T |-- phi: T proves phi directly (by application of a single rule) phi -| T: phi is proven by T phi --| T: phi is proven by T directly