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.

1. You must use the following character combinations from the left column to represent the sentential connectives and quantifiers identified on the right (you can copy and paste into the form fields if you don't know how to type them):

    ~   (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:

1. Line numbers must be surrounded with parentheses.
2. You must place each line of proof on a separate line.

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.