
Authors:
Stephen COOK and Michael SOLTYS
Title:Boolean Programs and Quantified Propositional Proof Systems
Pages:119129
File:bibtex
Abstract ( + )
We introduce the notion of Boolean programs, which provide more concise descriptions of Boolean functions than Boolean circuits. We characterize nonuniform PSPACE in terms of polynomial size families of Boolean programs. We then show how to use Boolean programs to witness quantifiers in the subsystems G_{1} and G_{1}^{*} of the proof system G for the quantified propositional calculus.

Authors:
Janis CIRULIS
Title:Positive Implicative BCKalgebras with Condition (S)
Pages:131133
File:bibtex
Abstract ( + )
As J.Meng, Y.B.Jun and S.M.Hong have recently proved the classes of algebras mentioned in the title are equal up to duality. We present here a short proof of their theorem.

Authors:
Vladimir V. RYBAKOV
Title:An explicit basis for rules admissible in modal system S4
Pages:135144
File:bibtex
Abstract ( + )
We find an explicit basis for all admissible rules of the modal logic S4. Our basis consists of an infinite sequence of rules which have compact and easy readable form and depend on increasing set of variables. This gives a basis for all quasiidentities valid in the free modal algebra F_{S4}(ω) of countable rank.

Authors:
Vladimir V. RYBAKOV, M. TERZILER and C. GENCER
Title:An essay on unification and inference rules for modal logics
Pages:145158
File:bibtex
Abstract ( + )
We study unification of formulas in modal logics and consider logics which are equivalent w.r.t. unification of formulas. A criterium is given for equivalence w.r.t. unification via existence or persistent formulas. A complete syntactic description of all formulas which are nonunifiable in wide classes of modal logics is given. Passive inference rules are considered, it is shown that in any modal logic over S4 there is a finite basis for passive rules.

Authors:
Ewa GRACZYNSKA and Zbigniew OZIEWICZ
Title:Birkhoff's theorems via tree operads
Pages:159178
File:bibtex
Abstract ( + )
Our aim is to present some of the main notion from universal algebra via tree operads. We propose an approach based on E. Marczewski ideas from 60'ties, connected with an abstract clone theory and the theory of tree operads and other operads as well as graphical notation and link diagrams and tangles. We are mainly interested in Birkhoff's like theorems, which shall be presented for some equational classes of algebras, such as: varieties and hypervarieties. An extended version of the paper has been submitted to the International Jornal of Theoretical Physics on 15 of August 1999.

Authors:
Piotr LUKOWSKI
Title:A reductive approach to Ldecidability
Pages:171177
File:bibtex
Abstract ( + )
The paper proposes some different approach to the Ldecidability testing it on intuitionistic logic. Traditionally, this problem has a ``deductive" solution, i.e. the set T^{1}, the complementation of the set of tautologies is defined by the axiom set and rules constructed from the deductive point of view. Although these axioms and rules are called ``rejected" and some of formulas appearing in them are preceded by symbol , all of them are taken de facto in some deductive sense, and other formulas are derived from axioms and rules by deduction. It seems that it would be more natural to obtain the set T^{1} by using of some reductive form of the logic conforming the principle that rejected formulas should result from reduction and not deduction. In our approach, T  the set of tautologies being naturally given by deductive logic, T^{1} is, also naturally, defined by the logic of reduction.