Undecidability of the completeness problem of modal logic
Undecidable varieties with solvable word problems. III (a semigroup variety).
Une généralisation de la théorie des types en -calcul
Une généralisation de la théorie des types en -calcul (II)
Une modélisation mathématique de la compréhension des énoncés additifs
Cet article fait suite à l'article paru dans le volume 113 de cette revue (D. Guin [15]) où nous avons mis en évidence certains processus cognitifs élémentaires dans l'activité de compréhension d'énoncés additifs, puis proposé une modélisation de la compréhension permettant de prendre en compte ces processus. Dans celle modélisation basée sur la notion d'opérateur, nous avons distingué deux étapes : la compréhension linguistique de l'énoncé et la réduction à un prototype. Nous utiliserons des formalismes...
Unification for nilpotent groups of class 2.
Unification in varieties of idempotent semigroups.
Unification of higher-order patterns modulo simple syntactic equational theories.
Uniform Space
In this article, we formalize in Mizar [1] the notion of uniform space introduced by André Weil using the concepts of entourages [2]. We present some results between uniform space and pseudo metric space. We introduce the concepts of left-uniformity and right-uniformity of a topological group. Next, we define the concept of the partition topology. Following the Vlach’s works [11, 10], we define the semi-uniform space induced by a tolerance and the uniform space induced by an equivalence relation....
Unsolvable systems of equations and proof complexity.
Unterstruktur-Invariante Formeln in der intuitionistischen Logik.
Using maximal ideals in the classification of MV-algebras
Using the possibility theory in fuzzy temporal reasoning
Validation sets in fuzzy logics
The validation set of a formula in a fuzzy logic is the set of all truth values which this formula may achieve. We summarize characterizations of validation sets of -fuzzy logics and extend them to the case of -fuzzy logics.
Validity up to complementation in graph theory
Veblen Hierarchy
The Veblen hierarchy is an extension of the construction of epsilon numbers (fixpoints of the exponential map: ωε = ε). It is a collection φα of the Veblen Functions where φ0(β) = ωβ and φ1(β) = εβ. The sequence of fixpoints of φ1 function form φ2, etc. For a limit non empty ordinal λ the function φλ is the sequence of common fixpoints of all functions φα where α < λ.The Mizar formalization of the concept cannot be done directly as the Veblen functions are classes (not (small) sets). It is done...
Very true operators on MTL-algebras
The main goal of this paper is to investigate very true MTL-algebras and prove the completeness of the very true MTL-logic. In this paper, the concept of very true operators on MTL-algebras is introduced and some related properties are investigated. Also, conditions for an MTL-algebra to be an MV-algebra and a Gödel algebra are given via this operator. Moreover, very true filters on very true MTL-algebras are studied. In particular, subdirectly irreducible very true MTL-algebras are characterized...
Vollständigkeit und Schnittelimination in der intuitionistischen Typenlogik.
Wajsberg algebras.
We present the basic theory of the most natural algebraic counterpart of the ℵ0-valued Lukasiewicz calculus, strictly logically formulated. After showing its lattice structure and its relation to C. C. Chang's MV-algebras we study the implicative filters and prove its equivalence to congruence relations. We present some properties of the variety of all Wajsberg algebras, among which there is a representation theorem. Finally we give some characterizations of linear, simple and semisimple algebras....
Weak Completeness Theorem for Propositional Linear Time Temporal Logic
We prove weak (finite set of premises) completeness theorem for extended propositional linear time temporal logic with irreflexive version of until-operator. We base it on the proof of completeness for basic propositional linear time temporal logic given in [20] which roughly follows the idea of the Henkin-Hasenjaeger method for classical logic. We show that a temporal model exists for every formula which negation is not derivable (Satisfiability Theorem). The contrapositive of that theorem leads...