Category theory based on combinatory logic.
Category-theoretic models of linear Abadi & Plotkin logic.
Cauchy-like functional equation based on a class of uninorms
Commuting is an important property in any two-step information merging procedure where the results should not depend on the order in which the single steps are performed. In the case of bisymmetric aggregation operators with the neutral elements, Saminger, Mesiar and Dubois, already reduced characterization of commuting -ary operators to resolving the unary distributive functional equations. And then the full characterizations of these equations are obtained under the assumption that the unary...
Cayley's Theorem
The article formalizes the Cayley's theorem saying that every group G is isomorphic to a subgroup of the symmetric group on G.
Centraliser dimension and universal classes of groups.
Characteristic of Rings. Prime Fields
The notion of the characteristic of rings and its basic properties are formalized [14], [39], [20]. Classification of prime fields in terms of isomorphisms with appropriate fields (ℚ or ℤ/p) are presented. To facilitate reasonings within the field of rational numbers, values of numerators and denominators of basic operations over rationals are computed.
Characterization of binary operations on the unit interval satisfying the generalized modus ponens inference rule.
Choice functions and well-orderings over the infinite binary tree
We give a new proof showing that it is not possible to define in monadic second-order logic (MSO) a choice function on the infinite binary tree. This result was first obtained by Gurevich and Shelah using set theoretical arguments. Our proof is much simpler and only uses basic tools from automata theory. We show how the result can be used to prove the inherent ambiguity of languages of infinite trees. In a second part we strengthen the result of the non-existence of an MSO-definable well-founded...
Choice sequences and Markov's principle
Church-Rosser property and decidability of monadic theories of unary algebras
Circumcenter, Circumcircle and Centroid of a Triangle
We introduce, using the Mizar system [1], some basic concepts of Euclidean geometry: the half length and the midpoint of a segment, the perpendicular bisector of a segment, the medians (the cevians that join the vertices of a triangle to the midpoints of the opposite sides) of a triangle. We prove the existence and uniqueness of the circumcenter of a triangle (the intersection of the three perpendicular bisectors of the sides of the triangle). The extended law of sines and the formula of the radius...
Classes of fuzzy filters of residuated lattice ordered monoids
The logical foundations of processes handling uncertainty in information use some classes of algebras as algebraic semantics. Bounded residuated lattice ordered monoids (monoids) are common generalizations of -algebras, i.e., algebras of the propositional basic fuzzy logic, and Heyting algebras, i.e., algebras of the propositional intuitionistic logic. From the point of view of uncertain information, sets of provable formulas in inference systems could be described by fuzzy filters of the corresponding...
Classical logic with some probability operators.
Classification of Maps by Their Membership in Maximal Clones That Contain Minimum and Complement
Combinatory logic and the ω-rule
Communication with www in Czech
This paper describes UIO, a multi–domain question–answering system for the Czech language that looks for answers on the web. UIO exploits two fields, namely natural language interface to databases and question answering. In its current version, UIO can be used for asking questions about train and coach timetables, cinema and theatre performances, about currency exchange rates, name–days and on the Diderot Encyclopaedia. Much effort have been made into making addition of a new domain very easy. No...
Commutativeness of Fundamental Groups of Topological Groups
In this article we prove that fundamental groups based at the unit point of topological groups are commutative [11].
Compacidad Y Decibilidad De Logicas Monadicas Con Cuantificadores Cardinales.
Compactness and Löwenheim-Skolem properties in categories of pre-institutions
The abstract model-theoretic concepts of compactness and Löwenheim-Skolem properties are investigated in the "softer" framework of pre-institutions [18]. Two compactness results are presented in this paper: a more informative reformulation of the compactness theorem for pre-institution transformations, and a theorem on natural equivalences with an abstract form of the first-order pre-institution. These results rely on notions of compact transformation, which are introduced as arrow-oriented generalizations...
Compactness in Metric Spaces
In this article, we mainly formalize in Mizar [2] the equivalence among a few compactness definitions of metric spaces, norm spaces, and the real line. In the first section, we formalized general topological properties of metric spaces. We discussed openness and closedness of subsets in metric spaces in terms of convergence of element sequences. In the second section, we firstly formalize the definition of sequentially compact, and then discuss the equivalence of compactness, countable compactness,...