-LIST LEFT * Principia Mathemematica Proof Checker * By Daniel J. O'Leary * Copyright (c) 1982 Daniel J. O'Leary * Reentered with permission from printouts by Dennis J. Darland - 2017 * * * Principia Mathathenatica Proof Checker * * By Dan J. O'Leary * * Copyright (c) 1982 DAniel J. O'Leary * * Re-entered with changes from printout * * by Dennis J. Darland * * Copyright (C) 2017 Dennis J. Darland * * This file is part of Dan J. O'Leary's proof checker for PM * * It is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by * the Free Software Foundation, either version 3 of the License, or * (at your option) any later version. * * It is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with it. If not, see . * DATE LAST CHANGED July 23, 1982 by O'Leary * Reentered starting June 2, 2017 by Darland * Dennis J. Daland making many changes. * * The Defined Functions come first. * The Program starts at the Label START * sub_line is the text into which thr substitution is made * subs is the string with the substitutions in it.' * Fill up the substitution table. * Start by setting it to the Identity Substitution * * DJD NOTES: * I have used mixed case - the original was all upper case. * Mostly Upper for Snobol4 keywords & labels. * Lover for user variables. * Also used '[' and ']' instead of '<' and '>'. * * 6/20/2017 DJD - Trying to make line numbers match. * Will initially br one off bcause of goto START which is necessary * * substitution(sub_line,subs)s1,s2,s3,n1 * DJD :(START) added - line numbers 1 large uniil :(START) F1 senvar = 'pqrstuv' F1.1 senvar LEN(1) . s1 = :F(F1.2) sub[s1] = s1 :(F1.1) * Now get the indicated substitution into the table. * First append a comma and a blank to show the end F1.2 subs = subs ', ' F1.3 subs (BREAK('/') . s1 ) '/' (BREAK(',') . s2) + ',' (SPAN(' ') . s3) :F(F1.4) sub[s1] = s2 subs s1 '/' s2 ',' s3 = :(F1.3) * * Now we actually make the substitution and print. F1.4 senvar = 'pqrstuv' num = '1234567' * Change the sentenial variables to numbers F1.5 senvar LEN(1) . s1 = :F(F1.7) num LEN(1) . n1 = F1.6 sub_line s1 = n1 :S(F1.6)F(F1.5) * Now replace the numbers by their substitutions F1.7 senvar = 'pqrstuv' num = '1234567' F1.8 senvar LEN(1) . s1 = :F(F1END) num LEN(1) . n1 = F1.9 sub_line n1 = sub[s1] :S(F1.9)F(F1.8) F1END substitution = sub_line :(RETURN) * * * skip(in),n1 F2 GE(in,0) :F(FRETURN) n1 = 0 F2.1 n1 = n1 + 1 page_out = F2END GE(n1,in) :F(F2.1)S(RETURN) * * * put_page() F3 spaces = 50 * DJD omition of 'PAGE = ' gets line numbers correct page_out = center(heading) page_out = page_out = DUPL(' ',spaces) ths_num page_out = DUPL(' ',spaces) date_pm skip(1) F3END page_lines = 10 :(RETURN) * * * arabic(in),n F4 arabic = roman_to_arabic[in] F4END NE(arabic,0) :S(RETURN)F(FRETURN) * * * DJD - GOT RID OF F5 - no need to limit printing. * * DJD - GOT RID OF F6 - REVERSE is built in. * * DJD - Will leave blank lines - they create line numbers * * implication(string) F7 string POS(0) 'C' | POS(0) 'E' :F(FRETURN) stack_count = 1 string POS(0) 'C' = '#' string POS(0) 'E' = '#' string = REVERSE(string) onech = LEN(1) . ch F7.1 string onech = :F(FRETURN) * If it is a sentential variable push it onto the stack. ch NOTANY('#NCAKE') :F(F7.2) stack[stack_count] = ch stack_count = stack_count + 1 :(F7.1) * If it is a unary connective pop, concatenate, and push. F7.2 ch 'N' :F(F7.3) stack[stack_count - 1] = stack[stack_count - 1] ch :(F7.1) * If it is a binary connective pop, pop, concat, and push. F7.3 ch any('CAKE') :F(F7.4) stack[stack_count - 2] = stack[stack_count - 2] + stack[stack_count - 1] + ch stack_count = stack_count - 1 :(F7.1) * If it is the "C" or "E" from the beginning we are done. F7.4 ch '#' :F(FRETURN) implication = REVERSE(stack[2]) '#' REVERSE(stack[1]) F7END :(RETURN) * * * Controls the spacing of line numbers and internal * line numbers to keep the proof left justified * sp(in) F8 sp = in ' ' sp parens :F(F8.2) * Internal line numbrs. They have a constant width of 7 * if they are used. Otherwise they are null. EQ(num_pf_lines,1) :F(F8.1) sp = :(RETURN) F8.1 * Right justify at line 7 sp '()' = sp = DUPL(' ',7 - SIZE(sp)) sp :(RETURN) * Line numbers F8.2 GE(in,10) :S(RETURN) F8END sp = ' ' sp :(RETURN) * * * center(in) F9 excess = page_width - SIZE(in) GT(excess,0) :F(FRETURN) EQ(remdr(excess,2),0) :S(F9.1)F(F9END) F9.1 center = DUPL(' ',excess / 2) in :(RETURN) F9END center = DUPL(' ',(excess + 1) / 2) in :(RETURN) * * * abs(in) F10 in = INTEGER(in) :F(FRETURN) abs = in abs = LT(in,0) -abs F10END :(RETURN) * * * cont_page() F11 spaces = 50 * WAS PAGE = page_out = page_out = center(heading) page_out = page_out = DUPL(' ',spaces) ths_num '(CONT.)' skip(1) F11END page_lines = 10 :(RETURN) -EJECT * * START DEFINE('initio()','INITIO1') initio() &STLIMIT = 1000000 &ERRLIMIT = 100 &TRIM = 1 &OUTPUT = 1 &INPUT = 1 &TRACE = 0 &DUMP = 1 &FTRACE = 0 * * theorem = TABLE(300,20) name = TABLE(220,10) line = TABLE(70,5) part = TABLE(32,4) sub = TABLE(10,10) roman_to_arabic = TABLE(5) roman_to_arabic['I'] = 1 roman_to_arabic['II'] = 2 roman_to_arabic['III'] = 3 stack = TABLE(8,2) pf_line = TABLE(32,2) * * mp_mark = POS(0) 'C' pm = (POS(0) '*1.01') + | (POS(0) '*2.33') + | (POS(0) '*3.01') + | (POS(0) '*3.02') + | (POS(0) '*4.01') + | (POS(0) '*4.02') + | (POS(0) '*4.34') ti = (POS(0) '*4.1') + | (POS(0) '*4.11') + | (POS(0) '*4.12') + | (POS(0) '*4.13') + | (POS(0) '*4.14') assump_mark = 'ASSUMP' conj_mark = POS(0) '*3.03' syll_mark = (POS(0) 'Syll') | (POS(0) 'SYLL') sub_mark = '/' se_mark = POS(0) 'SE' de_mark = POS(0) 'DE' | POS(0) 'DER' multi_line_pf_mark = '&' comment_mark = POS(0) '+' digit = SPAN('()#*.0123456789') digit_sp = SPAN(' ()#.0123456789') parens = ANY('()') * * page_num = 2 page_width = 80 page_length = 55 * * DEFINE('substitution(sub_line,subs)s1,s2,s3,n1','F1') DEFINE('skip(in)n1','F2') DEFINE('put_page()','F3') DEFINE('arabic(in)n','F4') * DJD Got Rid of OUTPUT_CONTROL() DEFINE('init_trace()','INTR') * DJD NOTE: There is built in 'REVERSE' funtion (do not need F6) DEFINE('implication(string)','F7') DEFINE('sp(in)','F8') DEFINE('center(in)excess','F9') DEFINE('abs(in)','F10') DEFINE('cont_page()','F11') * * * INIT_TRACE() * BLANK LINES for moved TRACE calls - line numbers * Read in a Title Page * skip(15) T1 title_page = center(INPUT) title_page 'END_OF_TITLE' :S(T2) page_out = title_page :(T1) T2 -EJECT * * * Read in a heading for each page. * Use it to determine the set of definitions to use. heading = center(INPUT) heading 'PRINCIPIA MATHEMATICA' :F(HEAD1) rep_mark = pm :(PRINT) HEAD1 heading 'THE THEORY OF IMPLICATION' :F(ERROR1) rep_mark = ti :(PRINT) * * * Get the date PRINT DATE_PM = DATE() * * * DJD REMOVED PRINTER CONTROL * * Read in the proof line abbreviation and the thesis. READ &INPUT = 1 * Set up the initial conditions on the proof * abbreviation to be read in and the full proof * to be generated. line_num = 0 num_pf_lines = 1 just = 0 READ4 proof = INPUT :F(TABLE_DJD) proof comment_mark :F(READ1) proof comment_mark = page_out = proof :(READ4) READ1 pf_line[1] = proof proof multi_line_pf_mark :F(READ2) just = 7 proof BREAK(multi_line_pf_mark) . num_pf_lines proof num_pf_lines multi_line_pf_mark = :F(ERROR1) pf_line[1] = proof pf_line_num = 1 READ3 pf_line_num = pf_line_num + 1 pf_line[pf_line_num] = INPUT GE(pf_line_num,num_pf_lines) :F(READ3) READ2 thesis = INPUT :F(ERROR1) thesis digit . ths_num * DJD PRINT CONTROL REMOVED put_page() * If &OUTPUT is not positive don't construct the proof. * DJD & OUTPUT is now always positive GE(&OUTPUT,1) :S(THM) * Put the thesis to be proved in the theorem table. thesis digit_sp REM . theorem[ths_num] * If the theorem has a blank there is a name. theorem[ths_num] BREAK(' ') . theorem[ths_num] + SPAN(' ') REM . name[ths_num] + :F(READ) name[ths_num] = '(' name[ths_num] ')' :(READ) -EJECT * * * Now analyze the proof line. * If the proof doesn't contain 'AX', 'DEF', or 'INF' it is a theorem. THM proof 'AX' | 'DEF' | 'INF' :S(AX) delim = ANY('+-;') * Put the thesis to be proved in the theorem table. thesis digit . thm_num SPAN(' ') . b thesis digit_sp REM . theorem[thm_num] * If the theorem has a blank there is a name. theorem[thm_num] BREAK(' ') . theorem[thm_num] + SPAN(' ') REM . name[thm_num] + :F(THM.1) name[thm_num] = '(' name[thm_num] ')' THM.1 page_out = thm_num ' ' theorem[thm_num] ' ' name[thm_num] skip(1) * * Print the proof abbreviation. page_out = 'PROOF ABBREVIATION' pf_line_num = 0 PF1 pf_line_num = pf_line_num + 1 page_out = pf_line[pf_line_num] GE(pf_line_num,num_pf_lines) :F(PF1) * * Print the full proof. skip(1) page_out = 'PROOF' page_lines = page_lines + num_pf_lines + 2 * Get the parts out of the proof line. pf_line_num = 0 PF2 pf_line_num = pf_line_num + 1 proof = pf_line[pf_line_num] GT(pf_line_num,num_pf_lines) :S(ERROR6) proof = proof '+' part_num = 0 LOOP1 part_num = part_num + 1 proof BREAK('+-;') . part[part_num] :F(THS) proof part[part_num] delim = :(LOOP1) * * * If the proof contains 'AX' it is an axiom. AX proof 'AX' :F(DEF) thesis digit . ax_num thesis digit_sp REM . theorem[ax_num] theorem[ax_num] BREAK(' ') . theorem[ax_num] + SPAN(' ') REM . NAME[ax_num] + :F(AX.1) name[ax_num] = '(' name[ax_num] ')' * Leave parens off axiom name in input AX.1 skip(2) page_out = ax_num ' ' theorem[ax_num] ' Pp. ' name[ax_num] :(READ) * * * If the proof contains 'DEF' it is a definition. DEF proof 'DEF' :F(INF) thesis digit . def_num thesis digit_sp REM . theorem[def_num] * If the definition has a blank there is a name. theorem[def_num] BREAK(' ') . theorem[def_num] + SPAN(' ') REM . name[def_num] + :F(DEF.1) * DJD Leave parens off name input!!! name[def_num] = '(' name[def_num] ')' * ABOVE LINE RE-COMMENTED 6/13/17 DJD DEF.1 skip(2) * LINE MISSING FROM BOTTOM OF PAGE DJD 6/12/17 - fixed 6/13/17 page_out = def_num ' ' theorem[def_num] ' Df. ' name[def_num] :(READ) * * * If the proof contains 'INF' just read in the words. * Note that '#' is an end of text marker. INF proof 'INF' :F(ERROR1) skip(2) INF.1 thesis '#' :S(INF.2) page_out = thesis thesis = INPUT :(INF.1) INF.2 thesis '#' = ' Pp.' page_out = thesis :(READ) -EJECT * * * Parse each part and construct the line. * First turn off input for efficiency. See Griswold, * Poage, and Polonsky section 11.5. THS &INPUT = 1 biggest_part_num = part_num - 1 * The line number is set to zero up at read, so that * it will be incremented through the whole proof as * each proof line is analyzed. * I wish to print the line numbers used in the proof * abbreviations. They are at the end of each proof * abbreviation and they contain left and right * parenthesis. They will be called internal line numbers. part_num = 0 int_line_num = '()' * DJD 6/19/17 - removed spaces around () above I had added * seemed to make no difference * cannot tell from printout. PARSE part_num = part_num + 1 EQ(part_num,biggest_part_num - 1) :F(PARSE1) part[biggest_part_num] parens :F(PARSE1) int_line_num = part[biggest_part_num] PARSE1 * Check for skip to a new page because the proof is too long. GE(page_lines,page_length) cont_page() line_num = line_num + 1 GT(part_num,biggest_part_num) :S(ERROR6) * The part must call for modus ponens, substitution, * replacement, syll, sub. Of EQ, * Or placing a previously proved theorem * on a line. The line to be proved must be in the * last part; all other single numbers are placements * on a line. part[part_num] mp_mark :S(MP) part[part_num] conj_mark :S(CONJ) part[part_num] assump_mark :S(ASSUMP) part[part_num] rep_mark :S(REP) part[part_num] syll_mark :S(SYLL) part[part_num] se_mark :S(SE) part[part_num] sub_mark :S(SUB) part[part_num] de_mark :S(DE) EQ(part_num,biggest_part_num) :F(PLACE)S(COMP) * * * Substutution rule * Get the theorem number SUB part[part_num] digit . thm_num SPAN(' ') . b :F(ERROR2) * Print the theorem and, if any, the substitutions. part[part_num] parens :F(SUB.1) line_num = line_num - 1 :(SUB.2) SUB.1 line[line_num] = theorem[thm_num] page_out = DUPL(' ',just) sp(line_num) line[line_num] + ' ' thm_num ' ' name[thm_num] SUB.2 part[part_num] thm_num b = page_out = DUPL(' ',just + 6) part[part_num] * Now perform the substitution and print the result. line[line_num + 1] = substitution(line[line_num], + part[part_num]) line_num = line_num + 1 page_out = sp(int_line_num) sp(line_num) line[line_num] ' SUB' page_lines = page_lines + 3 :(PARSE) * * MP * MODUS PONENS * CPQ, The antecedant p, and the consequent q. The proof * part gives us the antecedant only. The antecedant is * constructed first, then we back up through the proof to * the implication, and finally pull out the consequent. * First construct the antecedant. part[part_num] 'C' digit . thm_num * The implication could already be in the proof. This is * true iff the theorem number has left and right parens. thm_num parens :F(LMP4) * Back up through the proof until we get the antecedant. * Decrement the line number because we do not generate * a new line. line_num = line_num - 1 ant_num = line_num LMP5 line[ant_num] POS(0) theorem[thm_num] RPOS(0) :S(LMP1) ant_num = ant_num - 1 EQ(ant_num,0) :S(ERROR5)F(LMP5) * The implication is not already in the proof. LMP4 line[line_num] = theorem[thm_num] ant_num = line_num page_out = DUPL(' ',just) sp(line_num) line[line_num] + ' ' thm_num ' ' name[thm_num] page_lines = page_lines + 1 * Test for a substitution. part[part_num] '/' :F(LMP1) part[part_num] 'C' thm_num SPAN(' ') REM . temp page_out = DUPL(' ',just + 6) temp line[line_num + 1] = substitution(line[line_num],temp) line_num = line_num + 1 ant_num = line_num page_out = DUPL(' ',just) sp(line_num) line[line_num] + ' SUB' page_lines = page_lines + 2 * Now find the implication. LMP1 imp_num = line_num * The implication can be in one of three forms: CPQ, EPQ, or EQP. * In each case we know only p. When it may be EQP then the * length of q must be computed so that it may be skipped. * q itself is not known. * PAGE_OUT = 'line[ant_num] =' line[ant_num] * PAGE_OUT = 'ant_num = ' ant_num * LMP3 PAGE_OUT = 'line[imp_num] =' line[imp_num] * PAGE_OUT = 'imp_num = ' imp_num LMP3 line[imp_num] POS(0) ('C' | 'E') line[ant_num] REM . conclusion + :S(LMP2) line[imp_num] POS(0) ('E' arb . conclusion line[ant_num]) RPOS(0) + :S(LMP2) imp_num = GT(imp_num,1) imp_num - 1 :F(ERROR5)S(LMP3) * Now pull out the consequent. LMP2 line_num = line_num + 1 * PAGE_OUT = 'CONCLUSION = ' conclusion line[line_num] = line[imp_num] * Check the result. * Allow either 'C' or 'E' on the front. line[line_num] POS(0) ('C' | 'E') line[ant_num] = :S(LMP6) * This will allow p to be derived from EPQ and q. line[line_num] = implication(line[line_num]) line[line_num] '#' line[ant_num] = :F(ERROR5) LMP6 page_out = sp(int_line_num) sp(line_num) line[line_num] + ' MP: ' imp_num ', ' ant_num page_lines = page_lines + 1 :(PARSE) * * * Replacement rule * Get the definition number. REP part[part_num] digit . def_num temp = theorem[def_num] page_out = DUPL(' ',just + 6) temp ' Df. ' def_num + ' ' name[def_num] page_lines = page_lines + 1 * * replacement_spot = 1 spot = * Test for a roman numeral. part[part_num] 'I' :F(LREP1) part[part_num] BREAK('I') SPAN('I') . spot :F(ERROR3) part[part_num] spot = :F(ERROR3) replacement_spot = arabic(spot) :F(ERROR3) part[part_num] = TRIM(part[part_num]) * Test for a substitution. LREP1 part[part_num] sub_mark :F(LREP2) part[part_num] def_num SPAN(' ') = :F(ERROR3) temp = substitution(temp,part[part_num]) page_out = DUPL(' ',just + 9) part[part_num] page_out = DUPL(' ',just + 6) temp ' Df.' page_lines = page_lines + 2 LREP2 temp (BREAK('=') . lhs) '=' (REM . rhs) :F(ERROR3) line[line_num] = line[line_num - 1] * Assume the right side of the definition is to be replaced * by the left side. If not we reverse the right and left * sides of the definition and proceed. line[line_num] rhs :S(LREP6) s = rhs rhs = lhs lhs = s * Determine the place for the replacement. * If replacement spot is one, snobol4 * Will do the job automatically. * Use '#' to mark the places we don't want to touch. LREP6 EQ(replacement_spot,1) :S(LREP4) n = 0 LREP3 n = n + 1 line[line_num] rhs = '#' :F(ERROR3) EQ(n,replacement_spot - 1) :F(LREP3) LREP4 line[line_num] rhs = lhs :F(ERROR3) LREP5 line[line_num] '#' = rhs :S(LREP5) page_out = sp(int_line_num) sp(line_num) line[line_num] + ' REP ' spot page_lines = page_lines + 1 :(PARSE) * * * Place a previously proved theorem on a line * unless it is there already. It is iff the theorem' * number has left and right parens. If this is true * we also give back the new line number we got. PLACE part[part_num] parens :F(PLACE1) line_num = line_num - 1 :(PARSE) PLACE1 line[line_num] = theorem[part[part_num]] :F(ERROR4) page_out = sp(int_line_num) sp(line_num) line[line_num] + ' ' part[part_num] ' ' + name[part[part_num]] page_lines = page_lines + 1 :(PARSE) * * * This places an assumption on a proof line. ASSUMP part[part_num] 'ASSUMP' SPAN(' ') = :F(ERROR4) line[line_num] = part[part_num] page_out = sp(int_line_num) sp(line_num) line[line_num] + ' ASSUMP' page_lines = page_lines + 1 :(PARSE) * This is a binary rule which takes in previously proved * formulas of the form CPQ, CQR and gives as result CPR. SYLL * Get out the theorem numbers part[part_num] 'SYLL' SPAN(' ') digit . thm1 + SPAN(', ') digit . thm2 :F(ERROR7) * Back up through the proof until the theorems are found. back_up = line_num - 1 match = 0 SYLL1 line[back_up] POS(0) theorem[thm1] RPOS(0) :S(SYLL2) line[back_up] POS(0) theorem[thm2] RPOS(0) + :S(SYLL3)F(SYLL4) SYLL2 num_thm1 = back_up match = match + 1 :(SYLL4) SYLL3 num_thm2 = back_up match = match + 1 SYLL4 back_up = back_up - 1 EQ(match,2) :S(SYLL5) EQ(back_up,0) :F(SYLL1) SYLL5 thm1 = implication(line[num_thm1]) :F(ERROR7) thm2 = implication(line[num_thm2]) :F(ERROR7) thm1 BREAK('#') . ant1 '#' REM . cons1 thm2 BREAK('#') . ant2 '#' REM . cons2 cons1 ant2 :F(SYLL6) line[line_num] = 'C' ant1 cons2 :(SYLL7) SYLL6 ant1 cons2 :F(ERROR7) line[line_num] = 'C' ant2 cons1 SYLL7 page_out = sp(int_line_num) sp(line_num) line[line_num] + ' SYLL: ' num_thm1 ', ' num_thm2 page_lines = page_lines + 1 :(PARSE) * * * Substivity of equivalence' SE part[part_num] ':' :F(SEE) part[part_num] se_mark SPAN(' (') BREAK(':') . s1 + ':' BREAK(')') . s2 :F(ERROR9) * Get the theorem numbers out and print the theorems. s1 digit . thm_num_lhs s2 digit . thm_num_rhs lhs = theorem[thm_num_lhs] rhs = theorem[thm_num_rhs] page_out = DUPL(' ',just + 6) lhs ' ' thm_num_lhs ' : ' + rhs ' ' thm_num_rhs page_lines = page_lines + 1 sub_lhs = sub_rhs = * Test for substitutions on the lhs. s1 sub_mark :F(SE1) s1 thm_num_lhs SPAN(' ') = :F(ERROR9) sub_lhs = s1 lhs = substitution(lhs,sub_lhs) * Test for substitutions on the rhs. SE1 s2 sub_mark :F(SE2) s2 thm_num_rhs SPAN(' ') = :F(ERROR9) sub_rhs = s2 rhs = substitution(rhs,sub_rhs) * If there are substitutions, then print them and their result. SE2 EQ(SIZE(sub_lhs) + SIZE(sub_rhs),0) :S(SE3) page_out = DUPL(' ',just + 9) sub_lhs ' : ' sub_rhs page_out = DUPL(' ',just + 6) lhs ' : ' rhs page_lines = page_lines + 2 * Verify that the anrecedants and consequents match properly. SE3 lhs = implication(lhs) :F(ERROR9) rhs = implication(rhs) :F(ERROR9) lhs BREAK('#') . ant_lhs '#' REM . cons_lhs :F(ERROR9) rhs BREAK('#') . ant_rhs '#' REM . cons_rhs :F(ERROR9) ant_lhs cons_rhs :F(ERROR9) ant_rhs cons_lhs :F(ERROR9) * Now make the replacement. line[line_num] = line[line_num - 1] line[line_num] ant_lhs = cons_lhs :S(SE4) line[line_num] cons_lhs = ant_lhs :F(ERROR9) SE4 page_out = sp(int_line_num) sp(line_num) line[line_num] ' SE' page_lines = page_lines + 1 :(PARSE) * * SEE part[part_num] se_mark SPAN(' (') BREAK(')') . s1 :F(ERROR11) * Get the theorem number. s1 digit . thm_num thm = theorem[thm_num] page_out = DUPL(' ',just + 6) thm ' ' thm_num page_lines = page_lines + 1 * Test for implication. thm POS(0) 'E' :F(ERROR11) * Test for substitutions. s1 sub_mark :F(SEE1) s1 thm_num SPAN(' ') = :F(ERROR11) page_out = DUPL(' ',just + 9) s1 thm = substitution(thm,s1) page_out = DUPL(' ',just + 6) thm page_lines = page_lines + 2 SEE1 thm = implication(thm) :F(ERROR11) thm BREAK('#') . s1 '#' REM . s2 :F(ERROR11) * Make the replacement. * It is made in this order since the most common use is * to change NNP to P using EPNNP. line[line_num] = line[line_num - 1] line[line_num] s2 = s1 :S(SEE2) * If it didn't work, try the other way. line[line_num] s1 = s2 :F(ERROR11) SEE2 page_out = sp(int_line_num) sp(line_num) + line[line_num] ' SE' page_lines = page_lines + 1 page_lines = page_lines + 1 :(PARSE) * * * PM rule called "CONJ" * This is a binary rule which takes in previously proved * formulas and returns their conjunction. CONJ * Get out the theorem numbers. part[part_num] '*3.03' SPAN(' ') digit . thm1 + SPAN(', ') digit . thm2 :F(ERROR10) * Back up through the proof until the theorems are found. back_up = line_num - 1 match = 0 CONJ1 line[back_up] POS(0) theorem[thm1] RPOS(0) :S(CONJ2) line[back_up] POS(0) theorem[thm2] RPOS(0) + :S(CONJ3)F(CONJ4) CONJ2 num_thm1 = back_up match = match + 1 :(CONJ4) CONJ3 num_thm2 = back_up match = match + 1 CONJ4 back_up = back_up - 1 EQ(match,2) :S(CONJ5) EQ(back_up,0) :F(CONJ1) CONJ5 line[line_num] = 'K' line[num_thm1] line[num_thm2] page_out = sp(int_line_num) sp(line_num) line[line_num] + ' *3.03: ' num_thm1 ', ' num_thm2 page_lines = page_lines + 1 :(PARSE) * * * This rule takes a theorem of the form EPQ and returns * either CPQ or CQP (for DER). DE part[part_num] de_mark :F(ERROR12) part[part_num] POS(0) 'DER' :S(DE1) line[line_num] = line[line_num - 1] line[line_num] POS(0) 'E' = 'C' :F(ERROR12) page_out = sp(int_line_num) sp(line_num) line[line_num] ' DE' page_lines = page_lines + 1 :(PARSE) DE1 temp = implication(line[line_num - 1]) temp BREAK('#') . s1 '#' REM . s2 :F(ERROR12) line[line_num] = 'C' s2 s1 page_out = sp(int_line_num) sp(line_num) line[line_num] ' DER' page_lines = page_lines + 1 :(PARSE) * * * Compare the theorem proved with that which was read in. COMP thesis digit . thm_num * The line number which had been incremented in anticipation * of another inference rule. line_num = line_num - 1 * First see if this is the last line of the proof * or just of the proof abbreviation. part[part_num] (thm_num | 'PROP' | 'Prop') :S(COMP1) * Save the proved line for later use. theorem[part[part_num]] = line[line_num] :(PF2) COMP1 line[line_num] POS(0) theorem[thm_num] RPOS(0) :F(PROB) :(READ) PROB page_out = DUPL('*',60) page_out = 'The last line of the proof and the thesis' page_out = 'which was read in do not agree!' page_out = 'The program takes the thesis which was' page_out = 'read in to be correct;' page_out = thm_num ' ' theorem theorem[thm_num] page_out = DUPL('*',60) :(READ) * * * This section prints out theorems and definitions read in. TABLE_DJD ths_num = ' ' date_djd = DATE() heading = 'SUMMARY OF THEOREMS AND DEFINITIONS' put_page() theorems = CONVERT(theorem,'ARRAY') j = 0 i = 1 TABLE1 * In the next step failure could mean the end of the array. TABLE2 theorems[i,1] POS(0) '*' :F(TABLE3) page_out = theorems[i,1] DUPL(' ',8 - SIZE(theorems[i,1])) + theorems[i,2] ' ' name[theorems[i,1]] :F(END) j = j + 1 * See if the array has ended. If yes, finish. TABLE3 theorems[i,1] :F(END) i = i + 1 EQ(0,REMDR(j,50)) :F(TABLE2) cont_page() :(TABLE1) -EJECT * ERROR OUTPUT SECTION ERROR1 st_num = &LASTNO skip(2) page_out = DUPL('*',60) page_out = 'READ ERROR' page_out = 'PROOF IS ' proof page_out = 'THESIS IS ' thesis page_out = 'HEADING IS ' heading page_out = 'ST. NUM IS ' st_num :(READ) ERROR2 st_num = &LASTNO skip(2) page_out = DUPL('*',60) page_out = 'SUBSTITUTION ERROR' page_out = 'THESIS IS ' thesis page_out = 'P/N ' part_num ' ' part[part_num] page_out = 'L/N ' line_num ' ' line[line_num] page_out = 'ST. NUM IS ' st_num :(READ) ERROR3 st_num = &LASTNO skip(2) page_out = DUPL('*',60) page_out = 'REPLACEMENT ERROR' page_out = 'P/N ' part_num ' ' part[part_num] page_out = 'DEF ' def_num ' ' theorem[def_num] page_out = 'TEMP ' temp page_out = 'RHS ' rhs page_out = 'LHS ' lhs page_out = 'REPLACEMENT SPOT ' replacement_spot page_out = 'SPOT ' spot page_out = 'ST. NUM IS ' st_num :(READ) ERROR4 st_num = &LASTNO skip(2) page_out = DUPL('*',60) page_out = 'PLACE ERROR' page_out = 'L/N ' line_num page_out = 'P/N ' part_num page_out = 'PART ' part[part_num] page_out = 'ST. NUM IS ' st_num :(READ) ERROR5 st_num = &LASTNO skip(2) page_out = DUPL('*',60) page_out = 'MODUS PONENS ERROR' page_out = 'ST. NUM IS ' st_num page_out = 'IMP_NUM IS ' imp_num page_out = 'LINE[IMP_NUM] IS ' line[imp_num] page_out = 'ANT_NUM IS ' ant_num page_out = 'LINE[ANT_NUM] IS ' line[ant_num] :(READ) ERROR6 st_num = &LASTNO skip(2) page_out = DUPL('*',60) page_out = 'PF LINE OR PART ERROR' page_out = 'ST. NUM IS ' st_num :(READ) ERROR7 st_num = &LASTNO skip(2) page_out = DUPL('*',60) page_out = 'SYLL ERROR' page_out = 'THM1 IS ' thm1 page_out = 'THM2 IS ' thm2 page_out = 'ST. NUM IS ' st_num page_out = 'ANT1 IS ' ant1 page_out = 'CONS1 IS ' cons1 page_out = 'ANT2 IS ' ANT2 page_out = 'CONS2 IS ' cons2 :(READ) ERROR8 st_num = &LASTNO skip(2) page_out = DUPL('*',60) page_out = 'SE ERROR' page_out = 'ST. NUM IS ' st_num page_out = 'LINE IS ' LINE[LINE_NUM] page_out = 'LINE NUMBER IS ' LINE_NUM page_out = 'LHS ' lhs page_out = 'RHS ' rhs :(READ) ERROR9 st_num = &LASTNO skip(2) page_out = DUPL('*',60) page_out = 'SE ERROR' page_out = 'PART IS ' part[part_num] page_out = 'S1 IS ' s1 page_out = 'S2 IS ' s2 page_out = 'LHS ' lhs page_out = 'RHS ' rhs page_out = 'SUB_LHS IS ' sub_lhs page_out = 'SUB_RHS IS ' sub_rhs page_out = 'ST. NUM IS ' st_num :(READ) ERROR10 st_num = &LASTNO skip(2) page_out = DUPL('*',60) page_out = 'CONJ ERROR' page_out = 'THM1 IS ' thm1 page_out = 'THM2 IS ' thm2 page_out = 'ST. NUM IS ' st_num :(READ) ERROR11 st_num = &LASTNO skip(2) page_out = DUPL('*',60) page_out = 'SE (EQUIV.) ERROR' page_out = 'PART IS ' part[part_num] page_out = 'S1 IS ' s1 page_out = 'S2 IS ' s2 page_out = 'THM IS ' THM page_out = 'ST. NUM IS ' st_num :(READ) ERROR12 st_num = &LASTNO skip(2) page_out = DUPL('*',60) page_out = 'DE OR DER ERROR' page_out = 'PART IS ' part[part_num] page_out = 'S1 IS ' s1 page_out = 'S2 IS ' s2 page_out = 'ST. NUM IS ' st_num :(READ) INITIO1 INPUT('INPUT',5,4096,'data_in00.txt') OUTPUT('OUTPUT',6,4096,'data_out00.txt') OUTPUT('page_out',7,4096,'page_out00.txt') INITIO2 OUTPUT('debug_out',8,4096,'debug_out00.txt') :(RETURN) INTR TRACE('HEAD1','LABEL') TRACE('PRINT','LABEL') TRACE('READ','LABEL') TRACE('THM','LABEL') TRACE('THM.1','LABEL') TRACE('PF1','LABEL') TRACE('PF2','LABEL') TRACE('LOOP1','LABEL') TRACE('AX','LABEL') TRACE('AX1','LABEL') TRACE('INF','LABEL') TRACE('INF.1','LABEL') TRACE('INF.2','LABEL') TRACE('THS','LABEL') TRACE('PARSE','LABEL') TRACE('PARSE1','LABEL') TRACE('SUB','LABEL') TRACE('SUB.1','LABEL') TRACE('SUB.2','LABEL') TRACE('MP','LABEL') TRACE('LMP5','LABEL') TRACE('LMP4','LABEL') TRACE('LMP1','LABEL') TRACE('LMP3','LABEL') TRACE('LMP2','LABEL') TRACE('LMP6','LABEL') TRACE('REP','LABEL') TRACE('LREP1','LABEL') TRACE('LREP2','LABEL') TRACE('LREP6','LABEL') TRACE('LREP3','LABEL') TRACE('LREP4','LABEL') TRACE('LREP5','LABEL') TRACE('PLACE','LABEL') TRACE('PLACE1','LABEL') TRACE('ASSUMP','LABEL') TRACE('SYLL','LABEL') TRACE('SYLL1','LABEL') TRACE('SYLL2','LABEL') TRACE('SYLL3','LABEL') TRACE('SYLL4','LABEL') TRACE('SYLL5','LABEL') TRACE('SYLL6','LABEL') TRACE('SYLL7','LABEL') TRACE('SE','LABEL') TRACE('SE1','LABEL') TRACE('SE2','LABEL') TRACE('SE3','LABEL') TRACE('SE4','LABEL') TRACE('SEE','LABEL') TRACE('SEE1','LABEL') TRACE('SEE2','LABEL') TRACE('CONJ','LABEL') TRACE('CONJ1','LABEL') TRACE('CONJ2','LABEL') TRACE('CONJ3','LABEL') TRACE('CONJ4','LABEL') TRACE('CONJ5','LABEL') TRACE('DE','LABEL') TRACE('DE1','LABEL') TRACE('COMP','LABEL') TRACE('COMP1','LABEL') TRACE('TABLE_DJD','LABEL') TRACE('TABLE1','LABEL') TRACE('TABLE2','LABEL') TRACE('TABLE3','LABEL') TRACE('ERROR1','LABEL') TRACE('ERROR2','LABEL') TRACE('ERROR3','LABEL') TRACE('ERROR4','LABEL') TRACE('ERROR5','LABEL') TRACE('ERROR6','LABEL') TRACE('ERROR7','LABEL') TRACE('ERROR8','LABEL') TRACE('ERROR9','LABEL') TRACE('ERROR10','LABEL') TRACE('ERROR11','LABEL') TRACE('ERROR12','LABEL') TRACE('PROOF','VALUE') TRACE('THS_NUM','VALUE') TRACE('PF_LINE_NUM','VALUE') TRACE('PART_NUM','VALUE') TRACE('THESIS','VALUE') TRACE('AX_NUM','VALUE') TRACE('DEF_NUM','VALUE') TRACE('BIGGEST_PART_NUM','VALUE') TRACE('INT_LINE_NUM','VALUE') TRACE('LINE_NUM','VALUE') TRACE('ANT_NUM','VALUE') TRACE('IMP_NUM','VALUE') TRACE('REPLACEMENT_SPOT','VALUE') TRACE('SPOT','VALUE') TRACE('TEMP','VALUE') TRACE('RHS','VALUE') TRACE('LHS','VALUE') TRACE('S','VALUE') TRACE('N','VALUE') TRACE('BACK_UP','VALUE') TRACE('NUM_THM1','VALUE') TRACE('NUM_THM2','VALUE') TRACE('MATCH','VALUE') TRACE('THM1','VALUE') TRACE('THM2','VALUE') TRACE('ANT1','VALUE') TRACE('ANT2','VALUE') TRACE('CONS1','VALUE') TRACE('CONS2','VALUE') TRACE('THM_NUM_RHS','VALUE') TRACE('THM_NUM_LHS','VALUE') TRACE('SUB_RHS','VALUE') TRACE('SUB_LHS','VALUE') TRACE('PROOF','VALUE') TRACE('PROOF','VALUE') TRACE('PROOF','VALUE') INTREND TRACE('PROOF','VALUE') :(RETURN) END