Re: CoS and computability logic

Hi,

> I am sorry to disappoint you, but there is a "simple" counterexample to your
> conjecture "M=BKS".
>
> > *** Definition   System BKS is
> >
> >           t          (R,[T,U])       [(R,U),(T,V)]          f
> >     ai_ ------ ,   s --------- ,   m ------------- ,   aw_ --- ;
> >         [a,-a]       [(R,T),U]       ([R,T],[U,V])          a
> >

I think that this is the perfect occasion to advertise "CoS in Maude",
which is a very simple tool for implementing CoS systems,
so I will do so:

Since the system above does not have the contraction, it is a perfect
playground for experiments with simple examples for the Maude
implementation. The module attached below is a modification
(contraction is removed) of the module for KSn at

http://www.informatik.uni-leipzig.de/~ozan/maude_cos.html

The Maude System is available at the

http://maude.cs.uiuc.edu/

You have the following commands:

(1) For proof search:

search [b , [ a , - a ] ] =>+ tt .

(2) For search for arbitrary derivations, for instance:

search [b , [ a , - a ] ] =>+ [ b , a ] .

(3) To see the derivation steps

show path <state_number_displayed> .

(4) To observe all the possible rule applications to a structure:

search [b , [ a , - a ] ] =>1 R .


> Actually, I am not so sure about this. But I cannot really explain why.
I
> need more time to think about this.
>

I hope it can help.
Cheers.

-Ozan

*****************************
*****************************

mod BKSn is
  sort Unit .
  sort Atom .
  sort Structure .
  subsort Atom < Structure .
  subsort Unit < Structure .

  ops tt ff : -> Unit .
  op -_     : Atom -> Atom [ prec 50 ].
  op [_,_]  : Structure Structure -> Structure [assoc comm] .
  op {_,_}  : Structure Structure  -> Structure [assoc comm] .

  ops a b c d e : -> Atom .   *** positive atoms

  var R T U  V : Structure .
  var A : Atom .

    rl [interaction-down]  : [ A , - A ]       => tt .
    rl [switch]            : [ { R , T } , U ] => { [ R , U ] , T } .
    rl [medial]            : { [R,T] , [U,V] } => [ {R,U} , {T,V} ] .
    rl [weakenning-down]   :           A       => ff .

    rl [conjunction-unit]  :   { R , tt }      => R .
    rl [disjunction-unit]  :   [ R , ff ]      => R .
endm