
Authors:
A.V. FIGALLO, G. RAMON and S. SAAD
Title:iHPropositional Calculus
Pages:157162
File:bibtex
Abstract ( + )
Several authors have pointed out that the class of Nemitz's implicative semilattices are not the same as the class of Hilbert algebras with the property that for each pair of elements there exists its infimum, which we called Hilbert algebras with infimum. To the best of our knowledge, the first who realized this fact was Marsden in 1972. In a previous paper we have shown that the class of Hilbert algebras with infimum is equational and that the class of implicative semilattices is strictly contained in this variety. In this article, bearing in mind the relationship between the implicative semilattices and the {>,&}fragment of the intuitionistic propositional calculus, we describe a Hilbert style {>,&}propositional calculus weaker than the intuitionistic fragment and we show that the algebraic models of this new calculus are Hilbert algebras with infimum.

Authors:
Tarek Sayed AHMED and Basim SAMIR
Title:Neat Embeddings and Amalgamation
Pages:163171
File:bibtex
Abstract ( + )
We present a property of neat reducts commuting with forming subalgebras as a definability condition.

Authors:
David Gracia GARCIA
Title:An Example of a New Kind of Algebraizability
Pages:173185
File:bibtex
Abstract ( + )
We study the algebraization of a nonprotoalgebraic logic defined by Dosen. This logic, despite of being nonprotoalgebraic, has a theory which is algebraizable in a similar sense than a logic is, according to Blok and Pigozzi's notion.

Authors:
Norihiro KAMIDE
Title:An Equivalence Between Sequent Calculi for LinearTime Temporal Logic
Pages:187193
File:bibtex
Abstract ( + )
The equivalence between Kawai's sequent calculus LT_{ω} and BaratellaMasini's 2sequent calculus 2Sω is shown for the untilfree lineartime temporal logic. By using this equivalence, an alternative proof of the cutelimination theorems for LT_{ω} and 2Sω is obtained.

Authors:
Haroldo G. BENATTI and Ruy J.G.B. de QUEIROZ
Title:On the Descriptive Complexity of the Two Disjoint Paths Problem Over Undirected Graphs
Pages:195214
File:bibtex
Abstract ( + )
We are concerned with the problem of determining whether an undirected graph (V,E) with distinguished vertices s1, s2, t1, t2 has nodedisjoint paths from s1 to t1 and s2 to t2. We show that it is definable in least fixed point logic, meaning that it can be answered in polynomial time the question whether (G,s1,s2,t1,t2) is a yes instance of the problem by iteratively evaluating a firstorder formula on the graph until a fixedpoint is reached.