General Information The Logic Daemon is a proof checker designed to accompany Logic Primer ©2001 MIT Press.
How it works Enter your premises, conclusion, and proof in the form in the upper frame of the daemon window. Use commas to separate premises. Each line of proof should be formatted as shown in the text book, except for the changes noted below.
~ (not) & (and) v (or) [lower-case vee] -> (if-then)  <-> (iff)  @ (all)  $ (some) 
The program understands the parenthesis-dropping conventions. Thus PvQ->R is as acceptable as ((PvQ)->R)
Sample sequent and proof Here is a sample sequent and proof (containing a deliberate error) as it might be sent to the program to be checked:
@xFx, Fa->Q |- Q 1 (1) @xFx A 2 (2) Fa->Q A 1 (3) Fa 1@E 1,2(4) Q 2,3->E
IMPORTANT POINTS TO NOTE ABOUT THIS EXAMPLE:
Response and Feedback The response time of the program should be considerably less than one minute (1-2 seconds is normal from sites on the A&M campus), but this may vary if the network is especially heavily loaded. The messages generated by the program should be self-explanatory, but if you have any questions about them, or other bug reports, please send email to Colin Allen.