Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Resent-Date: Fri, 21 Oct 94 11:16:56 CET
Resent-From: KONTUR%PLTUMK11.BITNET@SEGATE.SUNET.SE
Resent-To: info-hol@leopard.cs.byu.edu, logic@cs.cornell.edu, 
           bra-types@cs.chalmers.se, isabelle-users@cl.cam.ac.uk
Date: Tue, 13 Sep 94 11:26:11 CET
From: KONTUR%PLTUMK11.BITNET@SEGATE.SUNET.SE
To: cblap@sun.leeds.ac.uk
Message-ID: <"swan.cl.cam.:208820:941021114714"@cl.cam.ac.uk>

FORWARDING THE ENGLISH-LANGUAGE TEXT GIVEN BELOW:

----------------------------Original message----------------------------
Oto poprawiona wersja tekstu niedawno wys\lanego do Pa\nstwa:

----------------------------Original message----------------------------

             A NOTE ABOUT NEEDED COMPUTER PROGRAMS


     I need some computer programs which may be realized by a
personal computer compatible with IBM AT (main processor: 80286,
numeric processor: none) and equipped by a system MS-DOS 5.0.
They should be programs, which:


1. verify, whether a formula is or is not a tautology of a given
   matrix - like TESTER does it (see [1], pp. 86-87);


2. solve tasks analogous to functional equations: let several
   formulae of a given sentential language be built of
   connectives (functors) enumerated in the definition of a
   given matrix and also of other connectives; then the program
   is to check, whether such other connectives may be defined in
   order to make the formulae tautologies (or non-tautologies)
   of the matrix - this might be perhaps a variant/extension of
   the previous program;


3. realize the algorithms of Jerzy Slupecki to define any binary
   truth-table with the help of some a priori established
   connectives: U's and S's (see  [10], p. 157), or - better! -
   C, R, and S (see [9], p. 157);


4. realize the algorithm dealt with in [3];


5. is similar (or even equivalent) to that one described very
   generally in [2];


6. seek:

   a) all ordinary [and (among them) all MATRIX] HOMOMORPHISMS
      from a given matrix into/onto another given matrix
      (included the case of AUTOMORPHISMS), morphisms defined as
      in [8] (def. 21, p. 21) for example;

   b) all MATRIX CONGRUENCES and all QUOTIENT MATRICES (see [12],
      pp. 140-141) of a given matrix;

   c) the CHARACTERISTIC SUBMATRICES OF THE [first and of the
      second] FUNCTIONAL MATRIX of a given matrix (see [8], def.
      29, p. 25);

   d) the PRODUCT of two given matrices (see [5], p. 174);

   e) the SUM of two given matrices (see [5], p. 174-175);

   f) every DECOMPOSITION of a given matrix INTO A PRODUCT of
      two other matrices (if such decompositions exist);

   g) every DECOMPOSITION of a given matrix INTO A SUM of
      two other matrices (if such decompositions exist);


7. verify, whether:

   a) a given matrix is an EMPTY one (see [6], the first
      theorem, p. 182;   [8], theorem 25, p. 25);

   b) a given matrix is "COMPLETE" or not (see [8], theorem 26,
      p. 26);

   c) two given matrices are EQUIVALENT or not (see [7], the
      section 5 of this article, pp. 162-163, or [8], theorem
      27* and following remarks, p. 28);

   d) two given matrices are CO-HOMOMORPHIC or not (see [8],
      def. 23, p. 21; the "effective method" is mentioned between
      theorem 22 and definition 24, p. 22);

   e) a given matrix is a STRONG (or a WEAK) MODEL of a
      sentential calculus also just given (the ÿeffective
      method" is mentioned in [4], lem. 3.1).


     It is very probable that some of the programs mentioned
above are not yet constructed. However, I'd be very fond of such
programs, wich deal with "matrices of Slupecki" (cf. [9]), that
is - with matrices, in which the designated values are: 1,...,k,
and the non-designated ones are: k+1,...,n.

     Of course, all the programs can deal only with those
matrices, which are finite and have reasonably small
cardinalities, not greater than n, where n equals to 10 (for
example, as in the case of TESTER in [1]).

I would like to achieve (if it is possible at all) the programs
through e-mailing in the European Academic Research Network. (My
network-address is the following one: KONTUR@PLTUMK11.BITNET)
Probably the programs could be sent as binary sets. In any case
the following information would be useful for me: how long are
the separate programs. (Before copying them onto my floppy disk
I must know, how many free kB's I need for this purpose.)


R e f e r e n c e s:

 [1] A. R. Anderson, N. D. Belnap Jr., ENTAILMENT. THE LOGIC OF
     RELEVANCE AND NECESSITY, vol. I, Princeton University Press
     1975.

 [2] R. T. Brady, A COMPUTER PROGRAM FOR DETERMINING MATRIX
     MODELS OF PROPOSITIONAL CALCULI, Logique et Analyse,
     yb. 19(1976), no. 74/75/76, pp. 233-253.

 [3] W. A. Carnielli, AN ALGORITHM FOR AXIOMATIZING AND THEOREM
     PROVING IN FINITE MANY-VALUED PROPOSITIONAL LOGICS, Logique
     et Analyse, yb. 28(1985), no. 112, pp. 363-368.

 [4] R. Harrop, ON THE EXISTENCE OF FINITE MODELS AND DECISION
     PROCEDURES FOR PROPOSITIONAL CALCULI, Proceedings of the
     Cambridge Philosophical Society, vol. 54(1958), no. 1, pp.
     1-13.

 [5] J. Kalicki, NOTE ON TRUTH-TABLES, The Journal of Symbolic
     Logic, vol. 15(1950), no. 3, pp. 174-181.

 [6] J. Kalicki, A TEST FOR THE EXISTENCE OF TAUTOLOGIES
     ACCORDING TO MANY-VALUED TRUTH-TABLES, The Journal of
     Symbolic Logic, vol. 15(1950), no. 3, pp. 182-184.

 [7] J. Kalicki, A TEST FOR THE EQUALITY OF TRUTH-TABLES, The
     Journal of Symbolic Logic, vol. 17(1952), no. 3, pp.
     161-163.

 [8] J. Los, O MATRYCACH LOGICZNYCH (= On logical matrices),
     Travaux de la Societe des Sciences et des Lettres de
     Wroclaw, ser. B, nr 19(1949), pp. 5-42; its translation
     into English is contained in [11].

 [9] J. Slupecki, PROOF OF AXIOMATIZABILITY OF FULL MANY-VALUED
     SYSTEMS OF CALCULUS OF PROPOSITIONS, Studia Logica, vol.
     29(1971), pp. 155-168.

[10] J. Slupecki, A CRITERION OF FULLNES OF MANY-VALUED SYSTEMS
     OF PROPOSITIONAL LOGIC, Studia Logica, vol. 30(1972), pp.
     153-157.

[11] D. E. Ulrich, MATRICES FOR SENTENTIAL CALCULI, Ph. D.
     diss., Wayne State University, 1967, Ann Arbor (University
     Microfilms) 1971 (numbers of pages mentioned by me in the
     present note refer only to [8]).

[12] R. Wojcicki, LECTURES ON PROPOSITIONAL CALCULI, Ossolineum,
     the Publishing House of the Polish Academy of Sciences,
     Wroclaw 1984.


     I am employed at the Chair of Logic of the Nicolaus
Copernicus University in Torun (Poland) and preparing a doctoral
dissertation about non-classical many-valued sentential calculi.
When not e-mailing, you can write to me using one of the
following two addresses:

the official one -

          Konrad Turzynski
          Katedra Logiki UMK
          ul. Fosa Staromiejska nr 3
          PL-87-100 Torun 1
          phone (48 56) from 26021 till 26025, internal: 133 or
          166

the private one -

          Konrad Turzynski
          ul. Kusocinskiego nr 8b m. 26
          PL-87-115 Torun 16
          phone (48 56) 482-825