implementing LPC in the Logic Lab

[Mark Tarver]

There is really a significant gain in brevity and clarity when logic rules are implemented in the Logic Lab extension.  My first port of call was the system for FOL in Logic, Proof and Computation.    The code is given at the end of this post.

It's hard to get a direct comparison with coding in Shen because sequent notation tends to be very spacey and the line count does not reflect the amount of code.  A better count is the K size of the file when whitespace is subtracted.  On that count the entirety of the FOL deduction rules in LPC are coded in 2K using the Logic Lab.  In Shen the original program takes 5K.

Expect to see the Logic Lab arrive next month.   Some time is still taken up with legal matters I'm afraid but we will get to the end of this.

Mark

(sequent hyp ()

   

     ______________

     P >> P;)

   

   (sequent vr1 ()

     P;

     ______________

     [P v Q];)

   

   (sequent vr2 ()

     Q;

     ______________

     [P v Q];)

   

   (sequent vl ()

     Q >> P;

     R >> P;

     ______________

     [Q v R] >> P;)

   

   (sequent &r ()

   

      P; Q;

      _____

      [P & Q];)

    

    (sequent &l ()

    

      P, Q >> R;

      __________

      [P & Q] >> R;)

      

    (sequent =>r ()

    

      P >> Q;

      _______

      [P => Q];)

      

     (sequent =>l ()

     

       [P => Q] >> P;

       ______________

       [P => Q] >> Q;)

       

     (sequent <=>r ()

     

       [[P => Q] & [Q => P]];

       ______________________

       [P <=> Q];)

       

     (sequent <=>l ()

     

       [[P => Q] & [Q => P]] >> R;

       ______________________

       [P <=> Q] >> R;) 

       

     (sequent ~r ()

     

       [P => falsum];

       ______________

       [~ P];)

       

     (sequent ~l ()

     

       [P => falsum] >> Q;

       ______________

       [~ P] >> Q;)                

   

     (sequent lemma (Q : prop)

   

       Q;

       Q >> P;

       _______

       P;)

       

     (sequent lem (P : prop)

      

       [P v [~ P]] >> Q;

       _________________

       Q;)

       

     (sequent exp ()

      

       falsum;

       _______

       P;)

       

     (define remove-nth

       {number --> (list A) --> (list A)}

        1 [_ | Y] -> Y

        N [X | Y] -> [X | (remove-nth (- N 1) Y)])  

       

     (sequent thin (N : number)

     

      let Hypotheses (remove-nth N Hypotheses)

      P;

      _________________________________________

      P;)

      

      (define exchange 

        {number --> number --> (list A) --> (list A)}

        M N X -> X     where (or (= M 0) (= N 0))

        1 N [X | Y] -> (let Z (nth N [X | Y])

                            [Z | (insert-nth X (- N 1) Y)])

        M 1 [X | Y] -> (let Z (nth M [X | Y])

                            [Z | (insert-nth X (- M 1) Y)])

        M N [X | Y] -> [X | (exchange (- M 1) (- N 1) Y)])

        

       (define insert-nth

         {A --> number --> (list A) --> (list A)}

          X 1 [_ | Y] -> [X | Y]

          X N [Y | Z] -> [Y | (insert-nth X (- N 1) Z)])                                      

      

      (sequent swap (M : number N : number)

      

        let Hypotheses (exchange M N Hypotheses)

        P;

        _________________________________________

        P;)

      

      (sequent =r ()

      

       _______

       [X = X];)

      

     (define replace

        {term --> term --> prop --> prop}

        Tm _ [all V P] -> [all V P]    where (== Tm V)

        Tm _ [exists V P] -> [exists V P]  where (== Tm V)

        Tm V [all X Y] -> [all X (replace Tm V Y)]

        Tm V [exists X Y] -> [exists X (replace Tm V Y)]

        Tm V [P v Q] -> [(replace Tm V P) v (replace Tm V Q)]

        Tm V [P & Q] -> [(replace Tm V P) & (replace Tm V Q)]

        Tm V [P => Q] -> [(replace Tm V P) => (replace Tm V Q)]

        Tm V [P <=> Q] -> [(replace Tm V P) <=> (replace Tm V Q)]

        Tm V [~ P] -> [~ (replace Tm V P)]

        Tm V [X = Y] -> [(replace* Tm V X) = (replace* Tm V Y)]

        Tm V [F | Terms] -> [F | (map (/. Term (replace* Tm V Term)) Terms)]  where (atomic? [F | Terms])

        _ _ P -> P)  

  

      (define replace*

        {term --> term --> term --> term}

        Tm V V -> Tm

        Tm V [Func | Tms] -> [Func | (map (/. Term (replace* Tm V Term)) Tms)]

        _ _ Term -> Term) 

        

       (sequent =l ()

      

       let PX/Y (replace X Y P)

       [X = Y] >> PX/Y;

       ________________________

       [X = Y] >> P;)       

           

     (sequent alll (T : term)

      

       let PX/T (replace X T P)

       PX/T, [all X P] >> Q;

       ________________________

       [all X P] >> Q;)

       

     (sequent allr (T : term)

      

       if (= (occurrences T Hypotheses) 0)

       let PX/T (replace X T P)

       PX/T;

       ________________________

       [all X P];)