Displaying similar documents to “A Model of Mizar Concepts - Unification”

Towards the Construction of a Model of Mizar Concepts

Grzegorz Bancerek (2008)

Formalized Mathematics

Similarity:

The aim of this paper is to develop a formal theory of Mizar linguistic concepts following the ideas from [14] and [13]. The theory here presented is an abstract of the existing implementation of the Mizar system and is devoted to the formalization of Mizar expressions. The base idea behind the formalization is dependence on variables which is determined by variable-dependence (variables may depend on other variables). The dependence constitutes a Galois connection between opposite poset...

On quasi-p-bounded subsets

M. Sanchis, A. Tamariz-Mascarúa (1999)

Colloquium Mathematicae

Similarity:

The notion of quasi-p-boundedness for p ∈ ω * is introduced and investigated. We characterize quasi-p-pseudocompact subsets of β(ω) containing ω, and we show that the concepts of RK-compatible ultrafilter and P-point in ω * can be defined in terms of quasi-p-pseudocompactness. For p ∈ ω * , we prove that a subset B of a space X is quasi-p-bounded in X if and only if B × P R K ( p ) is bounded in X × P R K ( p ) , if and only if c l β ( X × P R K ( p ) ) ( B × P R K ( p ) ) = c l β X B × β ( ω ) , where P R K ( p ) is the set of Rudin-Keisler predecessors of p.

Free Interpretation, Quotient Interpretation and Substitution of a Letter with a Term for First Order Languages

Marco Caminati (2011)

Formalized Mathematics

Similarity:

Fourth of a series of articles laying down the bases for classical first order model theory. This paper supplies a toolkit of constructions to work with languages and interpretations, and results relating them. The free interpretation of a language, having as a universe the set of terms of the language itself, is defined.The quotient of an interpreteation with respect to an equivalence relation is built, and shown to remain an interpretation when the relation respects it. Both the concepts...

Strong completeness of the Lambek Calculus with respect to Relational Semantics

Szabolcs Mikulás (1993)

Banach Center Publications

Similarity:

In [vB88], Johan van Benthem introduces Relational Semantics (RelSem for short), and states Soundness Theorem for Lambek Calculus (LC) w.r.t. RelSem. After doing this, he writes: "it would be very interesting to have the converse too", i.e., to have Completeness Theorem. The same question is in [vB91, p. 235]. In the following, we state Strong Completeness Theorems for different versions of LC.

Representation Theorem for Stacks

Grzegorz Bancerek (2011)

Formalized Mathematics

Similarity:

In the paper the concept of stacks is formalized. As the main result the Theorem of Representation for Stacks is given. Formalization is done according to [13].

Abstract Reduction Systems and Idea of Knuth-Bendix Completion Algorithm

Grzegorz Bancerek (2014)

Formalized Mathematics

Similarity:

Educational content for abstract reduction systems concerning reduction, convertibility, normal forms, divergence and convergence, Church- Rosser property, term rewriting systems, and the idea of the Knuth-Bendix Completion Algorithm. The theory is based on [1].

Quasi-analyticity in Carleman ultraholomorphic classes

Alberto Lastra, Javier Sanz (2010)

Annales de l’institut Fourier

Similarity:

We give a characterization for two different concepts of quasi-analyticity in Carleman ultraholomorphic classes of functions of several variables in polysectors. Also, working with strongly regular sequences, we establish generalizations of Watson’s Lemma under an additional condition related to the growth index of the sequence.

Relational Formal Characterization of Rough Sets

Adam Grabowski (2013)

Formalized Mathematics

Similarity:

The notion of a rough set, developed by Pawlak [10], is an important tool to describe situation of incomplete or partially unknown information. In this article, which is essentially the continuation of [6], we try to give the characterization of approximation operators in terms of ordinary properties of underlying relations (some of them, as serial and mediate relations, were not available in the Mizar Mathematical Library). Here we drop the classical equivalence- and tolerance-based...

Preliminaries to Classical First Order Model Theory

Marco Caminati (2011)

Formalized Mathematics

Similarity:

First of a series of articles laying down the bases for classical first order model theory. These articles introduce a framework for treating arbitrary languages with equality. This framework is kept as generic and modular as possible: both the language and the derivation rule are introduced as a type, rather than a fixed functor; definitions and results regarding syntax, semantics, interpretations and sequent derivation rules, respectively, are confined to separate articles, to mark...