Proof of the basic theorem on concept lattices in Isabelle/HOL

Download
2004-01-01
This paper presents a machine-checked proof of the Basic Theorem on Concept Lattices, which appears in the book "Formal Concept Analysis" by Canter and Wille, in the Isabelle/HOL Proof Assistant. As a by-product, the underlying lattice theory by Kammueller has been extended.
COMPUTER AND INFORMATION SCIENCES - ISCIS 2004, PROCEEDINGS

Suggestions

On the Krall-type polynomials on q-quadratic lattices
Alvarez-Nodarse, R.; Adiguzel, R. Sevinik (Elsevier BV, 2011-08-01)
In this paper, we study the Krall-type polynomials on non-uniform lattices. For these polynomials the second order linear difference equation, q-basic series representation and three-term recurrence relations are obtained. In particular, the q-Racah-Krall polynomials obtained via the addition of two mass points to the weight function of the non-standard q-Racah polynomials at the ends of the interval of orthogonality are considered in detail. Some important limit cases are also discussed. (C) 2011 Royal Net...
Formulation of a beam finite element for micro beams
Pehlivanoğlu, Yücel; Kadıoğlu, Fevzi Suat; Department of Mechanical Engineering (2018)
This study presents an Euler Bernoulli type micro-beam finite element for analyzing the size-dependent static and dynamic behavior of micro beams. The new element is based on Modified Couple Stress Theory (MCST). The governing equations of motion and the boundary conditions for the beam are derived and the conventional Galerkin technique is employed to formulate the finite element. The new element can be reduced to Classical Euler-Bernoulli beam element if the size-effect parameter in the element matrices i...
On the arithmetic of fibered surfaces
Kaba, Mustafa Devrim; Önsiper, Mustafa Hurşit; Department of Mathematics (2011)
In the first three chapters of this thesis we study two conjectures relating arithmetic with geometry, namely Tate and Lang’s conjectures, for a certain class of algebraic surfaces. The surfaces we are interested in are assumed to be defined over a number field, have irregularity two and admit a genus two fibration over an elliptic curve. In the final chapter of the thesis we prove the isomorphism of the Picard motives of an arbitrary variety and its Albanese variety.
Geometric invariant theory and Einstein-Weyl geometry
Kalafat, Mustafa (Elsevier BV, 2011-01-01)
In this article, we give a survey of geometric invariant theory for Toric Varieties, and present an application to the Einstein-Weyl geometry. We compute the image of the Minitwistor space of the Honda metrics as a categorical quotient according to the most efficient linearization. The result is the complex weighted projective space CP(1,1,2). We also find and classify all possible quotients. (C) 2011 Published by Elsevier GmbH.
Studies on non-weakly regular bent functions and related structures
Pelen, Rumi Melih; Özbudak, Ferruh; Department of Mathematics (2020)
Interest in bent functions over finite fields arises both from mathematical theory and practical applications. There has been lots of literature addressing various properties of bent functions. They have a number of applications consisting of coding theory, cryptography, and sequence designs. They’re divided into four subclasses: regular bent functions that are contained within the class of weakly regular bent functions that are contained within the class of dual-bent functions. Additionally, there are non-...
Citation Formats
B. Sertkaya and M. H. S. Oğuztüzün, “Proof of the basic theorem on concept lattices in Isabelle/HOL,” COMPUTER AND INFORMATION SCIENCES - ISCIS 2004, PROCEEDINGS, pp. 976–985, 2004, Accessed: 00, 2020. [Online]. Available: https://hdl.handle.net/11511/57233.