Weak focusing

From The Twelf Project

Jump to: navigation, search
This is Literate Twelf
Code: here
Status: %% OK %%
Output: here.

Contents

Polarized logic

polarity : type.			%name polarity S.
pos : polarity.
neg : polarity.

atm : polarity -> type.                 %name atm Q q.
prop : polarity -> type.                %name prop A.

atom : atm S -> prop S.
up : prop pos -> prop neg.
down : prop neg -> prop pos.
* : prop pos -> prop pos -> prop pos.   %infix right 10 *.
+ : prop pos -> prop pos -> prop pos.   %infix right 9 +.
-o : prop pos -> prop neg -> prop neg.  %infix right 8 -o.

%block bl_atmpos : block {qp:atm pos}.
%block bl_atmneg : block {qn:atm neg}.

Sequent calculus for polarized logic

Logic definition

A sequent is written

h1: hyp A1, ..., hn: hyp An |- conc A 
A1, ..., An |- A
hyp : prop S -> type.                   %name hyp H h.
conc : prop S -> type.                  %name conc D.

%block bl_hyp : some {S:polarity} {A:prop S} block {h:hyp A}.

init : hyp (atom Q) -> conc (atom Q).

upR : conc P
       -> conc (up P).
upL : (hyp P -> conc C)
       -> (hyp (up P) -> conc C).

downL : (hyp N -> conc C)
	    -> (hyp (down N) -> conc C).
downR : conc N
	 -> conc (down N).

*R : conc P1 -> conc P2 -> conc (P1 * P2).
*L : (hyp P1 -> hyp P2 -> conc C)
      -> (hyp (P1 * P2) -> conc C).

+R1 : conc P1 -> conc (P1 + P2).
+R2 : conc P2 -> conc (P1 + P2).
+L : (hyp P1 -> conc C)
      -> (hyp P2 -> conc C)
      -> (hyp (P1 + P2) -> conc C).

-oR : (hyp P -> conc N)
       -> (conc (P -o N)).
-oL : conc P
       -> (hyp N -> conc C)
       -> (hyp (P -o N) -> conc C).

%worlds (bl_atmpos | bl_atmneg | bl_hyp)
  (hyp A) (conc C).

Focused sequent calculus

Logic definition

Neutral sequent:

l1:left P1, ..., ln:left Pn |- right N
P1, ..., Pn |- N

Left-focused sequent:

l1:left P1, ..., ln:left Pn |- lfoc N1 N2
P1, ..., Pn [N1] |- N2

Right-focused sequent:

l1:left P1, ..., ln:left Pn |- rfoc P
P1, ..., Pn |- [P]

These can be generically expressed as:

l1:left P1, ..., ln:left Pn |- conseq C
P1, ..., Pn |- C
left : prop pos -> type.                %name left L l.

conclusion : type.                      %name conclusion C.
conseq : conclusion -> type.            %name conseq R.
conc-lfoc : prop neg -> prop neg -> conclusion.
conc-rfoc : prop pos -> conclusion.
conc-right : prop neg -> conclusion.

%abbrev rfoc = [P] conseq (conc-rfoc P).
%abbrev lfoc = [N][N'] conseq (conc-lfoc N N').
%abbrev right = [N] conseq (conc-right N).

%block bl_left : some {P:prop pos} block {l:left P}.

initR' : left (atom Qp) -> rfoc (atom Qp).
initL' : lfoc (atom Qn) (atom Qn).

upR' : rfoc P
        -> right (up P).
upL' : (left P -> right N)
        -> (lfoc (up P) N).

downR' : right N
          -> rfoc (down N).
downL' : (lfoc N N')
          -> (left (down N) -> right N').

*R' : rfoc P1
       -> rfoc P2
       -> rfoc (P1 * P2).
*L' : (left P1 -> left P2 -> right N')
       -> (left (P1 * P2) -> right N').

+R1' : rfoc P1
        -> rfoc (P1 + P2).
+R2' : rfoc P2 
        -> rfoc (P1 + P2).
+L' : (left P1 -> right N')
       -> (left P2 -> right N')
       -> (left (P1 + P2) -> right N').

-oR' : (left P -> right N) 
        -> (right (P -o N)).
-oL' : rfoc P
        -> (lfoc N N')
        -> (lfoc (P -o N) N').

%worlds (bl_atmpos | bl_atmneg | bl_left)
  (left P) (conseq C).   = (right N) (left N N') (rfoc P).

Cut admissibility

cut< : {N} lfoc N' N -> (lfoc N NC) -> lfoc N' NC -> type.
cut- : {N} right N -> (lfoc N NC) -> right NC -> type.
cut+ : {P} rfoc P -> (left P -> conseq C) -> conseq C -> type.
%mode cut< +N +D +E -F.
%mode cut- +N +D +E -F.
%mode cut+ +P +D +E -F.

Identity cuts

- : cut+ (atom Qp) (initR' D) ([l] initR' l) (initR' D).
- : cut< (atom Qn) (initL') (initL') (initL').

Principal cuts

- : cut- (up P) (upR' (D : rfoc P)) (upL' (E : left P -> right N)) F
     <- cut+ P D E (F : right N).

- : cut+ (down N) (downR' (D : right N)) 
     ([l:left (down N)] downL' (E l : lfoc N NC) l) G
     <- cut+ (down N) (downR' D) E (F : lfoc N NC)
     <- cut- N D F (G : right NC).

- : cut+ (P1 * P2) (*R' (D1 : rfoc P1) (D2 : rfoc P2)) 
     ([l:left (P1 * P2)] *L' (E l : left P1 -> left P2 -> right N) l) G
     <- ({l1:left P1}{l2: left P2} 
           cut+ (P1 * P2) (*R' D1 D2) ([l:left (P1 * P2)] E l l1 l2)
           (F l1 l2 : right N))
     <- ({l1:left P1} cut+ P2 D2 ([l2:left P2] F l1 l2) (F' l1 : right N))
     <- cut+ P1 D1 F' (G : right N).

- : cut+ (P1 + P2) (+R1' (D1 : rfoc P1))
     ([l:left (P1 + P2)] +L' (E1 l : left P1 -> right N) (E2 l) l) F
     <- ({l1:left P1}
           cut+ (P1 + P2) (+R1' D1) ([l:left (P1 + P2)] E1 l l1)
           (E1' l1 : right N))
     <- cut+ P1 D1 E1' (F : right N).

- : cut+ (P1 + P2) (+R2' (D2 : rfoc P2))
     ([l:left (P1 + P2)] +L' (E1 l) (E2 l : left P2 -> right N) l) F
     <- ({l2:left P2}
           cut+ (P1 + P2) (+R2' D2) ([l:left (P1 + P2)] E2 l l2)
           (E2' l2 : right N))
     <- cut+ P2 D2 E2' (F : right N).

- : cut- (N -o P) (-oR' (D1 : left N -> right P))
     (-oL' (E1 : rfoc N) (E2 : lfoc P NC)) F
     <- cut+ N E1 D1 (F1 : right P)
     <- cut- P F1 E2 (F : right NC).

Left commutative cuts

- : cut< N (upL' D) E (upL' F)
     <- ({l1} cut- N (D l1) E (F l1)).
- : cut- N (downL' D L) E (downL' F L)
     <- cut< N D E F.
- : cut- N (*L' D L) E (*L' F L)
     <- ({l1}{l2} cut- N (D l1 l2) E (F l1 l2)).
- : cut- N (+L' D1 D2 L) E (+L' F1 F2 L)
     <- ({l1} cut- N (D1 l1) E (F1 l1))
     <- ({l2} cut- N (D2 l2) E (F2 l2)).
- : cut< N (-oL' D1 D2) E (-oL' D1 F2)
     <- cut< N D2 E F2.

Right commutative cuts

- : cut+ P D ([l] initR' L) (initR' L).
- : cut+ P D ([l] initL') (initL').
- : cut+ P D ([l] upR' (E l)) (upR' F)
     <- cut+ P D ([l] E l) F.
- : cut+ P D ([l] upL' [l1] E l l1) (upL' F)
     <- ({l1} cut+ P D ([l] E l l1) (F l1)).
- : cut+ P D ([l] downR' (E l)) (downR' F)
     <- cut+ P D ([l] E l) F.
- : cut+ P D ([l] downL' (E l) L) (downL' F L)
     <- cut+ P D ([l] E l) F.
- : cut+ P D ([l] *R' (E1 l) (E2 l)) (*R' F1 F2)
     <- cut+ P D ([l] E1 l) F1
     <- cut+ P D ([l] E2 l) F2.
- : cut+ P D ([l] *L' ([l1][l2] E l l1 l2) L)
     (*L' ([l1][l2] F l1 l2) L)
     <- ({l1}{l2} cut+ P D ([l] E l l1 l2) (F l1 l2)).
- : cut+ P D ([l] +R1' (E l)) (+R1' F)
     <- cut+ P D ([l] E l) F.
- : cut+ P D ([l] +R2' (E l)) (+R2' F)
     <- cut+ P D ([l] E l) F.
- : cut+ P D ([l] +L' ([l1] E1 l l1) ([l2] E2 l l2) L)
     (+L' F1 F2 L)
     <- ({l1} cut+ P D ([l] E1 l l1) (F1 l1))
     <- ({l2} cut+ P D ([l] E2 l l2) (F2 l2)).
- : cut+ P D ([l] -oR' (E l)) (-oR' F)
     <- {l1} cut+ P D ([l] E l l1) (F l1).
- : cut+ P D ([l] -oL' (E1 l) (E2 l)) (-oL' F1 F2)
     <- cut+ P D ([l] E1 l) F1
     <- cut+ P D ([l] E2 l) F2.

%worlds (bl_atmpos | bl_atmneg | bl_left)
(cut< _ _ _ _)
(cut- _ _ _ _)
(cut+ _ _ _ _).

%total {(N1 N2 P3) [(D1 D2 D3) (E1 E2 E3)]}
(cut< N1 D1 E1 _)
(cut+ N2 D2 E2 _)
(cut- P3 D3 E3 _).

Corollary - unfocused cut

cut-unfoc+ : right (up P) -> (left P -> right N) -> right N -> type.
%mode cut-unfoc+ +D +E -F.

- : cut-unfoc+ D E F
     <- cut- (up P) D (upL' E) F.

%worlds (bl_atmpos | bl_atmneg | bl_left) (cut-unfoc+ _ _ _).
%total [] (cut-unfoc+ _ _ _).

cut-unfoc- : right A -> (left (down A) -> right C) -> right C -> type.
%mode cut-unfoc- +A +B -C.

- : cut-unfoc- D E F
     <- cut+ (down A) (downR' D) E F.

%worlds (bl_atmpos | bl_atmneg | bl_left) (cut-unfoc- _ _ _).
%total [] (cut-unfoc- _ _ _).

Identity

Eta expansion lemmas

eta- : {N:prop neg} ({N':prop neg} lfoc N N' -> right N') -> right N -> type.
eta+ : {P:prop pos} (rfoc P -> right N') -> (left P -> right N') -> type.
%mode eta- +N +R -R'.
%mode eta+ +P +R -R'.

%block bl_rfoc : some {P:prop pos} block {rf:rfoc P}.

- : eta+ (atom Qp) ([rf] R rf) ([l] R (initR' l)).

- : eta- (atom Qn) ([n'] [lf] R n' lf) (R (atom Qn) initL').

- : eta- (up P) ([n'] [lf] R n' lf) (R (up P) (upL' ([l] R' l)))
     <- eta+ P ([rf] upR' rf) ([l] R' l).

- : eta+ (down N) ([rf] R rf) ([l:left (down N)] R (downR' (R' l))) 
     <- ({l:left (down N)} eta- N ([n'] [lf] downL' lf l) (R' l)). 

- : eta+ (P1 * P2) ([rf] R rf) ([l] *L' ([l1] [l2] R'' l1 l2) l)
     <- ({rf1:rfoc P1} eta+ P2 ([rf2] R (*R' rf1 rf2)) ([l2] R' rf1 l2))
     <- ({l2:left P2} eta+ P1 ([rf1] R' rf1 l2) ([l1] R'' l1 l2)).

- : eta+ (P1 + P2) ([rf] R rf) (+L' R1 R2)
     <- eta+ P1 ([rf1] R (+R1' rf1)) ([l1:left P1] R1 l1 : right N)
     <- eta+ P2 ([rf1] R (+R2' rf1)) ([l2:left P2] R2 l2 : right N).

- : eta- (P1 -o N2) ([n'] [lf] R n' lf) (-oR' [l1] R1 l1)
     <- ({rf1:rfoc P1}
           eta- N2 ([n'] [lf2] R n' (-oL' rf1 lf2)) (R2  rf1))
     <- eta+ P1 ([rf1] R2 rf1) ([l1] R1 l1).

%worlds (bl_atmpos | bl_atmneg | bl_left | bl_rfoc)
  (eta- N R R') (eta+ P R R').

%total (N P) (eta- N _ _) (eta+ P _ _).

Identity corollaries

idp : {P:prop pos} (left P -> right (up P)) -> type.
%mode idp +P -R.

- : idp P R <- eta+ P ([rf] upR' rf) R.

%worlds (bl_atmpos | bl_atmneg | bl_left | bl_rfoc) (idp _ _).
%total [] (idp _ _).

idn : {N:prop neg} (left (down N) -> right N) -> type.
%mode idn +N -R.

- : idn N ([l] R l)
     <- ({l:left (down N)} eta- N ([qn] [lf] downL' lf l) (R l)). 

%worlds (bl_atmpos | bl_atmneg | bl_left | bl_rfoc) (idn _ _).
%total [] (idn _ _).

Soundness

sdR : right N -> conc N -> type.
sd+ : rfoc P -> conc P -> type.
sd- : lfoc N N' -> (hyp N -> conc N') -> type.
sdL : left P -> hyp P -> type.
%mode sdR +R -D.
%mode sd+ +R -D.
%mode sd- +R -D.
%mode sdL +L -H.

- : sd+ (initR' L) (init H)
     <- sdL L H.
- : sd- (initL') ([h] init h).
- : sdR (upR' R) (upR D)
     <- sd+ R D.
- : sd- (upL' [l] R l) ([h] upL ([hp] D hp) h)
     <- ({l} {hp} sdL l hp -> sdR (R l) (D hp)).
- : sd+ (downR' R) (downR D)
     <- sdR R D.
- : sdR (downL' R L) (downL ([hn] D hn) H)
     <- sd- R ([hn] D hn)
     <- sdL L H.
- : sd+ (*R' R1 R2) (*R D1 D2)
     <- sd+ R1 D1
     <- sd+ R2 D2.
- : sdR (*L' ([l1] [l2] R l1 l2) L12) (*L ([h1] [h2] D h1 h2) H12)
     <- ({l1} {h1} sdL l1 h1
           -> {l2} {h2} sdL l2 h2
           -> sdR (R l1 l2) (D h1 h2))
     <- sdL L12 H12.
- : sd+ (+R1' R1) (+R1 D1)
     <- sd+ R1 D1.
- : sd+ (+R2' R2) (+R2 D2)
     <- sd+ R2 D2.
- : sdR (+L' ([l1] R1 l1) ([l2] R2 l2) L) (+L ([h1] D1 h1) ([h2] D2 h2) H)
     <- ({l1} {h1} sdL l1 h1 -> sdR (R1 l1) (D1 h1))
     <- ({l2} {h2} sdL l2 h2 -> sdR (R2 l2) (D2 h2))
     <- sdL L H.
- : sdR (-oR' [l] R l) (-oR [h] D h)
     <- ({l} {h} sdL l h -> sdR (R l) (D h)).
- : sd- (-oL' R1 R2) ([h] -oL D1 ([h2] D2 h2) h)
     <- sd+ R1 D1
     <- sd- R2 ([h2] D2 h2).

%block bl_sdL : some {P:prop pos} block {l:left P} {h:hyp P} {_:sdL l h}.

%worlds (bl_atmpos | bl_atmneg | bl_sdL) (sdR _ _) (sd+ _ _) (sd- _ _) (sdL _ _).
%total [] (sdL _ _).
%total (R1 R2 R3) (sdR R1 _) (sd+ R2 _) (sd- R3 _).

Completeness

Unfocused admissibility

adm*R : right (up P1) -> right (up P2) -> right (up (P1 * P2)) -> type.
%mode adm*R +R1 +R2 -R.

- : adm*R (R1 : right (up P1)) (R2 : right (up P2)) R
     <- ({rf1:rfoc P1} eta+ P2 ([rf2:rfoc P2] upR' (*R' rf1 rf2)) 
           ([l2:left P2] R3 rf1 l2))
     <- ({l2:left P2} eta+ P1 ([rf1:rfoc P1] R3 rf1 l2) ([l1] R4 l1 l2))
     <- ({l2:left P2} cut-unfoc+ R1 ([l1:left P1] R4 l1 l2) (R5 l2))
     <- cut-unfoc+ R2 ([l2:left P2] R5 l2) R.

%worlds (bl_atmpos | bl_atmneg | bl_left) (adm*R _ _ _).
%total [] (adm*R _ _ _).

adm+R1 : right (up P1) -> right (up (P1 + P2)) -> type.
%mode +{P1:prop pos} +{P2:prop pos} +{R1:right (up P1)}
      -{R:right (up (P1 + P2))} (adm+R1 R1 R).

- : adm+R1 (R1 : right (up P1)) R
     <- eta+ P1 ([rf1:rfoc P1] upR' (+R1' rf1))
        (R1' : left P1 -> right (up (P1 + P2)))
     <- cut-unfoc+ R1 ([l1] R1' l1) R.

%worlds (bl_atmpos | bl_atmneg | bl_left) (adm+R1 _ _).
%total [] (adm+R1 _ _).

adm+R2 : right (up P2) -> right (up (P1 + P2)) -> type.
%mode +{P1:prop pos} +{P2:prop pos} +{R2:right (up P2)}
      -{R:right (up (P1 + P2))} (adm+R2 R2 R).

- : adm+R2 (R2 : right (up P2)) R
     <- eta+ P2 ([rf2:rfoc P2] upR' (+R2' rf2))
        (R2' : left P2 -> right (up (P1 + P2)))
     <- cut-unfoc+ R2 ([l2] R2' l2) R.

%worlds (bl_atmpos | bl_atmneg | bl_left) (adm+R2 _ _).
%total [] (adm+R2 _ _).

adm-oL : right (up P1)
	  -> (left (down N2) -> right N')
	  -> (left (down (P1 -o N2)) -> right N')
	  -> type.
%mode adm-oL +R1 +R2 -R.

- : adm-oL (R1 : right (up P1)) (R2 : left (down N2) -> right N')
     (R : left (down (P1 -o N2)) -> right N')
     <- ({l:left (down (P1 -o N2))} {rf1:rfoc P1}
           eta- N2 ([n][lf2] downL' (-oL' rf1 lf2) l) (R3 rf1 l : right N2))
     <- ({l} eta+ P1 ([rf1] R3 rf1 l) ([l1] R4 l l1))
     <- ({l} {l1} cut-unfoc- (R4 l l1) ([l2] R2 l2) (R5 l l1))
     <- ({l} cut-unfoc+ R1 ([l1] R5 l l1) (R l)).

%worlds (bl_atmpos | bl_atmneg | bl_left) (adm-oL _ _ _).
%total [] (adm-oL _ _ _).

Completeness

cph+ : hyp P -> left P -> type.
cph- : hyp N -> left (down N) -> type.
cp- : conc N -> right N -> type.
cp+ : conc P -> right (up P) -> type.
%mode cph+ +Hp -L.
%mode cph- +Hn -L.
%mode cp- +Dn -R.
%mode cp+ +Dp -R.

- : cp+ (init Hp) (upR' (initR' L))
     <- cph+ Hp L.
- : cp- (init Hn) (downL' (initL') L)
     <- cph- Hn L.

- : cp- (upR Dp) R
     <- cp+ Dp R.
- : cp- (upL ([hp] Dn1 hp) Hn) (downL' (upL' ([l] R1 l)) L)
     <- cph- Hn L
     <- ({hp:hyp P} {l:left P}
           cph+ hp l -> cp- (Dn1 hp) (R1 l)).
- : cp+ (upL ([hp] Dp1 hp) Hn) (downL' (upL' ([l] R1 l)) L)
     <- cph- Hn L
     <- ({hp:hyp P} {l:left P}
	   cph+ hp l -> cp+ (Dp1 hp) (R1 l)).

- : cp+ (downR Dn) (upR' (downR' R))
     <- cp- Dn R.
- : cp- (downL ([hn] Dn hn) Hp) (R L)
     <- cph+ Hp L
     <- ({hn:hyp N} {l:left (down N)}
           cph- hn l -> cp- (Dn hn) (R l)).
- : cp+ (downL ([hn] Dp hn) Hp) (R L)
     <- cph+ Hp L
     <- ({hn:hyp N} {l:left (down N)}
           cph- hn l -> cp+ (Dp hn) (R l)).

- : cp+ (*R Dp1 Dp2) R12
     <- cp+ Dp1 R1
     <- cp+ Dp2 R2
     <- adm*R R1 R2 R12.
- : cp- (*L ([hp1] [hp2] Dn hp1 hp2) Hp) (*L' ([l1] [l2] R l1 l2) L)
     <- cph+ Hp L
     <- ({hp1:hyp P1} {l1:left P1} cph+ hp1 l1
           -> {hp2:hyp P2} {l2:left P2} cph+ hp2 l2
           -> cp- (Dn hp1 hp2) (R l1 l2)).
- : cp+ (*L ([hp1] [hp2] Dp hp1 hp2) Hp) (*L' ([l1] [l2] R l1 l2) L)
     <- cph+ Hp L
     <- ({hp1:hyp P1} {l1:left P1} cph+ hp1 l1
           -> {hp2:hyp P2} {l2:left P2} cph+ hp2 l2
           -> cp+ (Dp hp1 hp2) (R l1 l2)).

- : cp+ (+R1 Dp1) R12
     <- cp+ Dp1 R1
     <- adm+R1 R1 R12.
- : cp+ (+R2 Dp2) R12
     <- cp+ Dp2 R2
     <- adm+R2 R2 R12.
- : cp- (+L ([h1] D1 h1) ([h2] D2 h2) H) (+L' R1 R2 L)
     <- cph+ H L
     <- ({h1}{l1} cph+ h1 l1 -> cp- (D1 h1) (R1 l1))
     <- ({h2}{l2} cph+ h2 l2 -> cp- (D2 h2) (R2 l2)).
- : cp+ (+L ([h1] D1 h1) ([h2] D2 h2) H) (+L' R1 R2 L)
     <- cph+ H L
     <- ({h1}{l1} cph+ h1 l1 -> cp+ (D1 h1) (R1 l1))
     <- ({h2}{l2} cph+ h2 l2 -> cp+ (D2 h2) (R2 l2)).

- : cp- (-oR [hp] Dn hp) (-oR' [l] R l)
     <- ({hp:hyp P} {l:left P}
           cph+ hp l -> cp- (Dn hp) (R l)).
- : cp- (-oL Dp1 ([hn2] Dn2 hn2) Hn) (R12 L)
     <- cph- Hn L
     <- cp+ Dp1 R1
     <- ({hn2:hyp N2} {l2:left (down N2)}
           cph- hn2 l2 -> cp- (Dn2 hn2) (R2 l2))
     <- adm-oL R1 ([l2] R2 l2) ([l] R12 l).
- : cp+ (-oL Dp1 ([hn2] Dp2 hn2) Hn) (R12 L)
     <- cph- Hn L
     <- cp+ Dp1 R1
     <- ({hn2:hyp N2} {l2:left (down N2)}
           cph- hn2 l2 -> cp+ (Dp2 hn2) (R2 l2))
     <- adm-oL R1 ([l2] R2 l2) ([l] R12 l).

%block bl_cph+ : some {P:prop pos} block {hp:hyp P} {l:left P} {_:cph+ hp l}.
%block bl_cph- : some {N:prop neg} block {hn:hyp N} {l:left (down N)} {_:cph- hn l}.

%worlds (bl_atmpos | bl_atmneg | bl_cph+ | bl_cph-)
   (cp- _ _) (cp+ _ _) (cph- _ _) (cph+ _ _).

%total [] (cph+ Hp _).
%total [] (cph- Hn _).
%total (Dn Dp) (cp- Dn _) (cp+ Dp _).

Translating into focused logic

A simple proof which is isomorphic in the unfocused and focused system, establishing |- a * b -o b * a for positive a and b.

%abbrev ' = [q] atom q.
r0 : {a:atm pos} {b:atm pos} right (' a * ' b -o up (' b * ' a))
   = [a] [b] -oR' ([lab] *L' ([la] [lb] upR' (*R' (initR' lb) (initR' la))) lab).
d0 : {a:atm pos} {b:atm pos} conc (' a * ' b -o up (' b * ' a))
   = [a] [b] -oR ([hab] *L ([ha] [hb] upR (*R (init hb) (init ha))) hab).
%query 1 * {a}{b} sdR (r0 a b) (D0 a b).
Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)

%query 1 * {a:atm pos} {b:atm pos} sdR (r0 a b) (D0 a b). ---------- Solution 1 ---------- D0 = [q:atm pos] [q1:atm pos] -oR ([h:hyp (atom q * atom q1)] *L ([h1:hyp (atom q)] [h2:hyp (atom q1)] upR (*R (init h2) (init h1))) h). ____________________________________________

%% OK %%
%query 1 * {a}{b} cp- (d0 a b) (R0 a b).
Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)

%query 1 * {a:atm pos} {b:atm pos} cp- (d0 a b) (R0 a b). ---------- Solution 1 ---------- R0 = [q:atm pos] [q1:atm pos] -oR' ([l:left (atom q * atom q1)] *L' ([l1:left (atom q)] [l2:left (atom q1)] upR' (*R' (initR' l2) (initR' l1))) l). ____________________________________________

%% OK %%

Reducing the number of proofs

This first example is already in "focused form" - invertible rules are applied only "before" upR is applied to prove |- (a + b) -> up (a + b)

%query 1 *
   {a: atm pos}{b: atm pos} 
   cp- (-oR ([h: hyp (atom a + atom b)]
		    +L ([ha: hyp (atom a)] upR (+R1 (init ha)))
		       ([hb: hyp (atom b)] upR (+R2 (init hb))) h))
            (D a b).
Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)

%query 1 * {a:atm pos} {b:atm pos} cp- (-oR ([h:hyp (atom a + atom b)] +L ([ha:hyp (atom a)] upR (+R1 (init ha))) ([hb:hyp (atom b)] upR (+R2 (init hb))) h)) (D a b). ---------- Solution 1 ---------- D = [q:atm pos] [q1:atm pos] -oR' ([l:left (atom q + atom q1)] +L' ([l1:left (atom q)] upR' (+R1' (initR' l1))) ([l1:left (atom q1)] upR' (+R2' (initR' l1))) l). ____________________________________________

%% OK %%

This a proof of the same sequent, but upR is applied before +L, which is fine in the unfocused system but not in the focused system, where upR starts a focusing phase and makes it impossible to apply invertible rules like +L. Translation produces the same focused proof from these two different unfocused proofs.

%query 1 *
   {a: atm pos}{b: atm pos} 
   cp- (-oR ([h: hyp (atom a + atom b)] 
		    upR (+L ([ha: hyp (atom a)] +R1 (init ha))
			    ([hb: hyp (atom b)] +R2 (init hb)) h)))
            (D a b).
Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)

%query 1 * {a:atm pos} {b:atm pos} cp- (-oR ([h:hyp (atom a + atom b)] upR (+L ([ha:hyp (atom a)] +R1 (init ha)) ([hb:hyp (atom b)] +R2 (init hb)) h))) (D a b). ---------- Solution 1 ---------- D = [q:atm pos] [q1:atm pos] -oR' ([l:left (atom q + atom q1)] +L' ([l1:left (atom q)] upR' (+R1' (initR' l1))) ([l1:left (atom q1)] upR' (+R2' (initR' l1))) l). ____________________________________________

%% OK %%

Forward and backward chaining

Finally, consder the following unfocused sequent proof. The proof proceeds in what we generally consider a "forward-chaining" manner, using the hypothesis (atom A) to obtain the hypothesis (atom B), which is then used to obtain the hypothesis (atom C), which is then used to obtain the hypothesis (atom D), which is finally used to finish.

implies-proof =
   [A: atm neg][B: atm neg][C: atm neg][D: atm neg]
   -oR (downL [ha: hyp (atom A)]
   -oR (downL [hab: hyp (down (atom A) -o (atom B))]
   -oR (downL [hbc: hyp (down (atom B) -o (atom C))]
   -oR (downL [hcd: hyp (down (atom C) -o (atom D))] 
    (-oL (downR (init ha)) 
     ([hb: hyp (atom B)]
      -oL (downR (init hb))
      ([hc: hyp (atom C)]
       -oL (downR (init hc))
       ([hd: hyp (atom D)] init hd) 
       hcd)
      hbc)
     hab))))).

Because negative polarity forces search to be goal directed, translating this proof into the focused system will flip the order in which the implications are considered, and no facts (beyond the four in the implication) will ever be added to the context.

%query 1 * 
   {a: atm neg}{b: atm neg}{c: atm neg}{d: atm neg}
   cp- (implies-proof a b c d) _.
Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)

%query 1 * {a:atm neg} {b:atm neg} {c:atm neg} {d:atm neg} cp- (implies-proof a b c d) (R1 a b c d). ---------- Solution 1 ---------- Empty Substitution. ____________________________________________

%% OK %%

Finally, we can show the proof of a successful attempt to prove right (A -o (A -o B) -o (B -o C) -o C) in the weakly focused system. In general, this could cause an infinite loop as Twelf has no problem with deriving multiple copies of the same fact, but here we use all negative atoms, and the resulting backward-chaining semantics corresponds nicely to Twelf's built-in backward-chaining semantics.

%solve p : 
   {a: atm neg}{b: atm neg}{c: atm neg}
   right (down (' a)
          -o down (down (' a) -o ' b) 
            -o down (down (' b) -o ' c) -o ' c).
Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)

%solve {a:atm neg} {b:atm neg} {c:atm neg} conseq (conc-right (down (atom a) -o down (down (atom a) -o atom b) -o down (down (atom b) -o atom c) -o atom c)). OK p : {a:atm neg} {b:atm neg} {c:atm neg} conseq (conc-right (down (atom a) -o down (down (atom a) -o atom b) -o down (down (atom b) -o atom c) -o atom c)) = [a:atm neg] [b:atm neg] [c:atm neg] -oR' ([l:left (down (atom a))] -oR' ([l1:left (down (down (atom a) -o atom b))] -oR' ([l2:left (down (down (atom b) -o atom c))] downL' (-oL' (downR' (downL' (-oL' (downR' (downL' initL' l)) initL') l1)) initL') l2))).

%% OK %%


Personal tools