Prof. Pliuskevicius Regimantas

was staying in St.Petersburg from 9.06.1997 to 9.07.1997

Wednesday, 2 July, 1997

14:30

Seminar of Laboratory of Mathematical Logic

Saturation Method for Linear Temporal First Order Logic

ABSTRACT

The report presents a reasoning system - saturation method - for a restricted first order linear temporal logic with "next" and "always". The most attractive property of saturation method consists in that it allows to built derivations uniformly both for a finitary complete and finitary incomplete first order linear temporal logic.

          Application for participation in the EIMI program

                      TETE-A-TETE IN RUSSIA

    I. Western participant(s)

       1) last name         Pliuskevicius
       2) given name(s)     Regimantas
       3) citizenship       LITHUANIA
       4) degree, title(s)  Ph.D., Professor
       5) affiliation
       6) position          Senior Scientist
       7) mailing address   Group of Mathematical Logic
                            Inst.Math. & Informatics
                            Akademijos 4, VILNIUS 2600
                            LITHUANIA

       8) e-mail address    regis@ktl.mii.lt
       9) phone number      +370-2-359511
      10) FAX number        +370-2-359209

    II. Russian participant(s)

       1) family name        Orevkov
       2) given name         Vladimir
       3) patronymic         Pavlovich
       4) degree, title(s)   Doctor of Phys.-Math. Sciences
       5) affiliation
       6) position           Leading Scientist
       7) mailing address    Laboratory of Mathematical Logic
                             V.A.Steklov Mathematical Institute
                             at St.Petersburg, Fontanka 27
                             191011, St.Petersburg
       8) e-mail address     orevkov@pdmi.ras.ru
       9) phone number        218-8107
      10) FAX number         +7-812-3105377

   III. Subject and form of proposed joint work (a few phrases)

We plan to investigation the question of the cut elimination in modal
and temporal logics. In particular, we intend to consider a new type
of finitary calculus for a restricted first order linear temporal logic.
Regimantas Pliuskevicius also plan to take part in the logical seminar
of PDMI.


    IV. Desired duration  one month in the period
        from  10 January  to  10 February.