Try   HackMD

LJT (G4ip) proof search

Originally invented by Roy Dyckhoff in Contraction-free sequent calculi for intuitionistic logic. G4ip is the sequent calculus derived from G3ip.

Also see an implementation by Michel Levy: http://teachinglogic.liglab.fr/
I traced down the code from the file preuve.ml ("proof" in French) in the DN1 variant.


Let context

Γ=Γ0Γ1Γ2Γ3, where

  • Γ1
    is a set of atoms,
  • Γ2
    is a set of clauses of the form
    bc
    where
    b
    is an atom,
  • Γ3
    is a set of clauses of the form
    (bd)c
    ,
  • Γ0
    is a set of formula of no restrictions.

Given a w.f.f.

a, decide whether
ΓNJa
. Usually initially
Γ=
.
Also give a witness if it is derivable.

Algorithm

  • If
    aΓ
    : Conclude "derivable" (
    assum
    ).
  • If one of below conditions holds:
    1. Γ0
      (
      L
      ), or
    2. there is some
      xΓ
      such that
      xaΓ
      , or
    3. Γ0
      contains either
      _a
      or
      a_
      (
      L;assum
      ),
    Conclude "derivable".

    Remark: modus ponens always holds by structural induction on

    x.

  • Else, Try to pattern match
    (Γ0,a)
    :
    • If
      a
      is of the form
      xy
      , apply
      R
      .
    • If
      a
      is of the form
      xy
      , apply
      R
      .

      Remark: after this stage,

      a can only be
      , an atom, or a disjunction.

    • If
      Γ0
      is non-empty, pick an element and pattern match:
      • an atom: Move it to
        Γ1
        and recurse.
      • a conjunction: Apply
        L
        .
      • a disjunction: Apply
        L
        .
      • an implication
        y=gb
        :
        Let
        Γ0=(Γ0{y})
        , prove
        gba
        as follows:
        1. Prove
          Γ0Γ1..3g
          , and then
        2. Prove (
          Γ0{b})Γ1..3a
          .

        Why? It resembles MP, but I cannot find a term to describe this process.

        If either step is not derivable, pattern match
        g
        and rewrite accordingly,
        • an atom: move
          y
          to
          Γ2
          and recurse.
        • a conjunction: apply
          L
          . Lemma p10
        • a disjunction: apply
          L
          . Lemma p11
        • an implication: move it to
          Γ3
          and recurse.
        • : remove
          y
          and recurse. (why?)
    • Else
      Γ0
      is empty. Try proceeding with the following steps in order.
      • Collect
        {p:pΓ1,pbΓ2}
        . If it is non-empty, apply
        L0
        on an element. If a proof fails, repeat this step on the remaining of them.
      • If
        Γ3
        is non-empty, pick an element in
        Γ3
        and apply
        L→→
        . Lemma p13
      • If
        a
        is a disjunction, apply
        R
        on either side.

        Remark: By the disjunction property, a disjunction is derivable if and only if either branch is derivable.

      • None of the above applies (
        a
        is
        or an atom).
        Conclude "not derivable".

        Remark: it is already not the case that

        aΓ.

To apply a rule, to prove a statement, or to move/remove an element to a set means that to re-enter the procedure with the resulting context

Γ=i=0..3Γi and formula.

The original algorithm describes everything as multisets for proving total correctness, but it seems that ordinary sets or lists suffices in practice.

Appendix

There are 8 proof rules in LJ. They are

assum,
L
,
L
,
R
,
L
,
R
,
L
,
R
.

The 4 rules replacing the problematic

L are as follows:

Γ,P,BEΓ,P,PBE(L0)with P atomic

Γ,D,BCDΓ,BEΓ,(CD)BE(L→→)

Γ,CDBEΓ,(CD)BE(L)

Γ,CB,DBEΓ,(CD)BE(L)

The witness can be collected from the path an input has undergone recursively.

Some lemmas are used to convert the sequent calculus back to natural deduction proofs. They are listed below, naming after variables found in the original code:

  • p10:
    (cd)bc(db)
  • p11:
    (cd)bdb
    (only the second branch)
  • p13:
    (cd)bdb
    (only the second branch)

Questions:

  1. Roy's paper did not give an explicit deciding procedure. Why this order of backtracking?
  2. Will it always terminate?
  3. When it rejects, how to prove that it has tried all paths?