All a b c d e f g h i j k l m n o p q r s t u v w x y z Other

Previous Page 45 Next

Displaying 881 – 900 of 1313

Showing per page

Summable Family in a Commutative Group

Roland Coghetto (2015)

Formalized Mathematics

Hölzl et al. showed that it was possible to build “a generic theory of limits based on filters” in Isabelle/HOL [22], [7]. In this paper we present our formalization of this theory in Mizar [6]. First, we compare the notions of the limit of a family indexed by a directed set, or a sequence, in a metric space [30], a real normed linear space [29] and a linear topological space [14] with the concept of the limit of an image filter [16]. Then, following Bourbaki [9], [10] (TG.III, §5.1 Familles sommables...

Sur la réfutabilité

Jean-Pierre Barthélémy (1974)

Cahiers de Topologie et Géométrie Différentielle Catégoriques

Sur la théorie élémentaire des groupes libres

Frédéric Paulin (2002/2003)

Séminaire Bourbaki

Sela a annoncé une solution complète d’un problème de Tarski, qui demanda vers 1945 quels sont les groupes de type fini qui ont la même théorie élémentaire qu’un groupe libre. Nous discuterons des travaux de Remeslennikov, Kharlampovich-Myasnikov, Sela, Champetier-Guirardel et autres sur la structure des groupes limites (les groupes de type fini qui sont “limites”de groupes libres, ou encore, qui ont la même théorie universelle qu’un groupe libre). Nous indiquerons quelques outils utilisés par Sela...

Sur les éléments de construction de la logique mathématique

M. Schönfinkel (1990)

Mathématiques et Sciences Humaines

Il s'agit de présenter l'article de Schönfinkel «Über die Bausteine der mathematischen Logik», préparé pour la publication (1924) par H. Behmann, d'après une conférence de Schönfinkel en 1920, qui fonde ce que Curry nommera «la logique combinatoire». L'objectif principal du travail de Schönfinkel est l'élimination générale des variables (propositionnelles, prédicatives, individuelles), grâce à l'usage de plusieurs «fonctions particulières». On trouvera ici : (1) une introduction à l'article de Schönfinkel,...

Symmetric implicational restriction method of fuzzy inference

Yiming Tang, Wenbin Wu, Youcheng Zhang, Witold Pedrycz, Fuji Ren, Jun Liu (2021)

Kybernetika

The symmetric implicational method is revealed from a different perspective based upon the restriction theory, which results in a novel fuzzy inference scheme called the symmetric implicational restriction method. Initially, the SIR-principles are put forward, which constitute optimized versions of the triple I restriction inference mechanism. Next, the existential requirements of basic solutions are given. The supremum (or infimum) of its basic solutions is achieved from some properties of fuzzy...

(T, ⊥, N) fuzzy logic.

Y. Xu, J. Lin, Da Ruan (2001)

Mathware and Soft Computing

To investigate more reasonable fuzzy reasoning model in expert systems as well as more effective logical circuit in fuzzy control, a (T, ⊥, N) fuzzy logic is proposed in this paper by using T-norm, ⊥-norm and pseudo-complement N as the logical connectives. Two aspects are discussed: (1) some concepts of (T, ⊥, N) fuzzy logic are introduced and some properties of (T, ⊥, N) fuzzy logical formulae are discussed. (2) G-fuzzy truth (falsity) of (T, ⊥, N) fuzzy logical formulae are investigated and also...

Taclets: a new paradigm for constructing interactive theorem provers.

Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Andreas Roth, Philipp Rümmer, Steffen Schlager (2004)

RACSAM

Frameworks for interactive theorem proving give the user explicit control over the construction of proofs based on meta languages that contain dedicated control structures for describing proof construction. Such languages are not easy to master and thus contribute to the already long list of skills required by prospective users of interactive theorem provers. Most users, however, only need a convenient formalism that allows to introduce new rules with minimal overhead. On the the other hand, rules...

Tarski Geometry Axioms – Part II

Roland Coghetto, Adam Grabowski (2016)

Formalized Mathematics

In our earlier article [12], the first part of axioms of geometry proposed by Alfred Tarski [14] was formally introduced by means of Mizar proof assistant [9]. We defined a structure TarskiPlane with the following predicates: of betweenness between (a ternary relation), of congruence of segments equiv (quarternary relation), which satisfy the following properties: congruence symmetry (A1), congruence equivalence relation (A2), congruence identity (A3), segment construction (A4), SAS (A5), betweenness...

Currently displaying 881 – 900 of 1313