Displaying 41 – 60 of 118

Showing per page

Independent axiom systems for nearlattices

João Araújo, Michael Kinyon (2011)

Czechoslovak Mathematical Journal

A nearlattice is a join semilattice such that every principal filter is a lattice with respect to the induced order. Hickman and later Chajda et al independently showed that nearlattices can be treated as varieties of algebras with a ternary operation satisfying certain axioms. Our main result is that the variety of nearlattices is 2 -based, and we exhibit an explicit system of two independent identities. We also show that the original axiom systems of Hickman as well as that of Chajda et al are...

Induction and decision procedures.

Deepak Kapur, Jürgen Giesl, Mahadevan Subramaniam (2004)

RACSAM

Mechanization of inductive reasoning is an exciting research area in artificial intelligence and automated reasoning with many challenges. An overview of our work on mechanizing inductive reasoning based on the cover set method for generating induction schemes from terminating recursive function definitions and using decision procedures is presented. This paper particularly focuses on the recent work on integrating induction into decision procedures without compromising their automation.

Isomorphisms of Direct Products of Cyclic Groups of Prime Power Order

Hiroshi Yamazaki, Hiroyuki Okazaki, Kazuhisa Nakasho, Yasunari Shidama (2013)

Formalized Mathematics

In this paper we formalized some theorems concerning the cyclic groups of prime power order. We formalize that every commutative cyclic group of prime power order is isomorphic to a direct product of family of cyclic groups [1], [18].

Isomorphisms of Direct Products of Finite Commutative Groups

Hiroyuki Okazaki, Hiroshi Yamazaki, Yasunari Shidama (2013)

Formalized Mathematics

We have been working on the formalization of groups. In [1], we encoded some theorems concerning the product of cyclic groups. In this article, we present the generalized formalization of [1]. First, we show that every finite commutative group which order is composite number is isomorphic to a direct product of finite commutative groups which orders are relatively prime. Next, we describe finite direct products of finite commutative groups

Isomorphisms of Direct Products of Finite Cyclic Groups

Kenichi Arai, Hiroyuki Okazaki, Yasunari Shidama (2012)

Formalized Mathematics

In this article, we formalize that every finite cyclic group is isomorphic to a direct product of finite cyclic groups which orders are relative prime. This theorem is closely related to the Chinese Remainder theorem ([18]) and is a useful lemma to prove the basis theorem for finite abelian groups and the fundamental theorem of finite abelian groups. Moreover, we formalize some facts about the product of a finite sequence of abelian groups.

Les schémas mentaux : représenter et maintenir une connaissance apprise

Denis Pierre (1997)

Mathématiques et Sciences Humaines

Nous nous intéressons à l'apprentissage à partir d'exemples et à la résolution de problème dans un univers évolutif représenté par une base de connaissances incomplète. Nous formalisons un cadre de représentation de connaissances susceptible d'être élaboré et critiqué par des humains comme par des machines. Cette représentation des connaissances est appelée théorie semi-empirique car cette forme de théorie n'est pas complètement axiomatique. Nous avons formalisé la gestion de la croissance incrémentale...

Normal Subgroup of Product of Groups

Hiroyuki Okazaki, Kenichi Arai, Yasunari Shidama (2011)

Formalized Mathematics

In [6] it was formalized that the direct product of a family of groups gives a new group. In this article, we formalize that for all j ∈ I, the group G = Πi∈IGi has a normal subgroup isomorphic to Gj. Moreover, we show some relations between a family of groups and its direct product.

On Rough Subgroup of a Group

Xiquan Liang, Dailu Li (2009)

Formalized Mathematics

This article describes a rough subgroup with respect to a normal subgroup of a group, and some properties of the lower and the upper approximations in a group.

Currently displaying 41 – 60 of 118