## Search

Now showing items 1-10 of 18

#### An Elementary Proof of Strong Normalization for Atomic F

(Uniwersytet Łódzki. Katedra Logiki i Metodologii Nauk, 2016)

We give an elementary proof (in the sense that it is formalizable in Peano arithmetic)
of the strong normalization of the atomic polymorphic calculus F_{at} (a
predicative restriction of Girard’s system F).

#### Irredundant Decomposition of Algebras into One-Dimensional Factors

(Wydawnictwo Uniwersytetu Łódzkiego, 2016)

We introduce a notion of dimension of an algebraic lattice and, treating such a lattice as the congruence lattice of an algebra, we introduce the dimension of an algebra, too. We define a star-product as a special kind of ...

#### Preserving Filtering Unification by Adding Compatible Operations to Some Heyting Algebras

(Wydawnictwo Uniwersytetu Łódzkiego, 2016)

We show that adding compatible operations to Heyting algebras and to commutative residuated lattices, both satisfying the Stone law ¬x ⋁ ¬¬x = 1, preserves filtering (or directed) unification, that is, the property that ...

#### Interpolation in Normal Extensions of the Brouwer Logic

(Wydawnictwo Uniwersytetu Łódzkiego, 2016)

The Craig interpolation property and interpolation property for deducibility are considered for special kind of normal extensions of the Brouwer logic.

#### On Direct Limit Closed Classes of Algebras

(Wydawnictwo Uniwersytetu Łódzkiego, 2016)

Axiomatic classes of algebras of a given type which are closed with respect to direct limits are studied in this paper.

#### Decomposition of Congruence Modular Algebras into Atomic, Atomless Locally Uniform and Anti-Uniform Parts

(Wydawnictwo Uniwersytetu Łódzkiego, 2016)

We describe here a special subdirect decomposition of algebras with modular congruence lattice. Such a decomposition (called a star-decomposition) is based on the properties of the congruence lattices of algebras. We ...

#### Characterization of Birkhoff’s Conditions by Means of Cover-Preserving and Partially Cover-Preserving Sublattices

(Wydawnictwo Uniwersytetu Łódzkiego, 2016)

In the paper we investigate Birkhoff’s conditions (Bi) and (Bi*). We prove that a discrete lattice L satisfies the condition (Bi) (the condition (Bi*)) if and only if L is a 4-cell lattice not containing a cover-preserving ...

#### Monadic Fragments of Intuitionistic Control Logic

(Wydawnictwo Uniwersytetu Łódzkiego, 2016)

We investigate monadic fragments of Intuitionistic Control Logic (ICL), which is obtained from Intuitionistic Propositional Logic (IPL) by extending language of IPL by a constant distinct from intuitionistic constants. In ...

#### An Alternative Natural Deduction for the Intuitionistic Propositional Logic

(Wydawnictwo Uniwersytetu Łódzkiego, 2016)

A natural deduction system NI, for the full propositional intuitionistic logic, is proposed. The operational rules of NI are obtained by the translation from Gentzen’s calculus LJ and the normalization is proved, via ...

#### Simple Decision Procedure for S5 in Standard Cut-Free Sequent Calculus

(Wydawnictwo Uniwersytetu Łódzkiego, 2016)

In the paper a decision procedure for S5 is presented which uses a cut-free sequent calculus with additional rules allowing a reduction to normal modal forms. It utilizes the fact that in S5 every formula is equivalent to ...