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

Page 1

Displaying 1 – 10 of 10

Showing per page

Object-Free Definition of Categories

Marco Riccardi (2013)

Formalized Mathematics

Category theory was formalized in Mizar with two different approaches [7], [18] that correspond to those most commonly used [16], [5]. Since there is a one-to-one correspondence between objects and identity morphisms, some authors have used an approach that does not refer to objects as elements of the theory, and are usually indicated as object-free category [1] or as arrowsonly category [16]. In this article is proposed a new definition of an object-free category, introducing the two properties:...

On global induction mechanisms in a μ -calculus with explicit approximations

Christoph Sprenger, Mads Dam (2003)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

We investigate a Gentzen-style proof system for the first-order μ -calculus based on cyclic proofs, produced by unfolding fixed point formulas and detecting repeated proof goals. Our system uses explicit ordinal variables and approximations to support a simple semantic induction discharge condition which ensures the well-foundedness of inductive reasoning. As the main result of this paper we propose a new syntactic discharge condition based on traces and establish its equivalence with the semantic...

On global induction mechanisms in a μ-calculus with explicit approximations

Christoph Sprenger, Mads Dam (2010)

RAIRO - Theoretical Informatics and Applications

We investigate a Gentzen-style proof system for the first-order μ-calculus based on cyclic proofs, produced by unfolding fixed point formulas and detecting repeated proof goals. Our system uses explicit ordinal variables and approximations to support a simple semantic induction discharge condition which ensures the well-foundedness of inductive reasoning. As the main result of this paper we propose a new syntactic discharge condition based on traces and establish its equivalence with the semantic...

On Multiset Ordering

Grzegorz Bancerek (2016)

Formalized Mathematics

Formalization of a part of [11]. Unfortunately, not all is possible to be formalized. Namely, in the paper there is a mistake in the proof of Lemma 3. It states that there exists x ∈ M1 such that M1(x) > N1(x) and (∀y ∈ N1)x ⊀ y. It should be M1(x) ⩾ N1(x). Nevertheless we do not know whether x ∈ N1 or not and cannot prove the contradiction. In the article we referred to [8], [9] and [10].

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.

On sequent calculi for intuitionistic propositional logic

Vítězslav Švejdar (2006)

Commentationes Mathematicae Universitatis Carolinae

The well-known Dyckoff's 1992 calculus/procedure for intuitionistic propositional logic is considered and analyzed. It is shown that the calculus is Kripke complete and the procedure in fact works in polynomial space. Then a multi-conclusion intuitionistic calculus is introduced, obtained by adding one new rule to known calculi. A simple proof of Kripke completeness and polynomial-space decidability of this calculus is given. An upper bound on the depth of a Kripke counter-model is obtained.

On Square-Free Numbers

Adam Grabowski (2013)

Formalized Mathematics

In the article the formal characterization of square-free numbers is shown; in this manner the paper is the continuation of [19]. Essentially, we prepared some lemmas for convenient work with numbers (including the proof that the sequence of prime reciprocals diverges [1]) according to [18] which were absent in the Mizar Mathematical Library. Some of them were expressed in terms of clusters’ registrations, enabling automatization machinery available in the Mizar system. Our main result of the article...

Ordered Rings and Fields

Christoph Schwarzweller (2017)

Formalized Mathematics

We introduce ordered rings and fields following Artin-Schreier’s approach using positive cones. We show that such orderings coincide with total order relations and give examples of ordered (and non ordered) rings and fields. In particular we show that polynomial rings can be ordered in (at least) two different ways [8, 5, 4, 9]. This is the continuation of the development of algebraic hierarchy in Mizar [2, 3].

Currently displaying 1 – 10 of 10

Page 1