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

Download

index.pdf

Date

2004-01-01

Author

Sertkaya, B
Oğuztüzün, Mehmet Halit S.

Metadata

Show full item record

This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Item Usage Stats

124
views

0
downloads

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.

URI

https://hdl.handle.net/11511/57233

Journal

COMPUTER AND INFORMATION SCIENCES - ISCIS 2004, PROCEEDINGS

DOI

https://doi.org/10.1007/978-3-540-30182-0_98

Collections

Department of Computer Engineering, Article

Suggestions

OpenMETU
Core

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.
Convergence performance of the approximate factorization methods with multi-block implicit boundary conditions at hypersonic speeds Koca, Melikşah; Eyi, Sinan; Department of Aerospace Engineering (2022-9) This thesis study presents convergence characteristics of the implicit approximate factorization methods at hypersonic flow conditions and with 2-dimensional and 3-dimensional geometries. The efficiency of the implicit boundary conditions at block interfaces for the multi-block grids is investigated for different approximate factorization methods. Standard Alternating Direction Implicit (ADI) method, Diagonal Dominant Alternating Direction Implicit method (DDADI) with and without Huang’s sub-iteration corre...
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.

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.