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

Download

index.pdf

Date

2003

Author

Sertkaya, Barış

Metadata

Show full item record

Item Usage Stats

191
views

0
downloads

Formel Concept Analysis is an emerging field of applied mathematics based on a lattice-theoretic formalization of the notions of concept and conceptual hierarchy. It thereby facilitates mathematical thinking for conceptual data analysis and knowledge processing. Isabelle, on the other hand, is a generic interactive theory development environment for implementing logical formalisms. It has been instantiated to support reasoning in several object-logics. Specialization of Isabelle for Higher Order Logic is called Isabelle/HOL. Our long term is to formalize the theory of Formal Concept Analysis in Isabelle/HOL. This will provide a mechanized theory for researchers who want to prove their own theorems with utmost precision, and for developers who want to design knowledge processing algorithms. The speccific accomplishment of this thesis is a machinechecked version of the proof of the Basic Theorem of Concept Lattices, which appears in the book "Formal Concept Analysisé by Ganter and Wille. As a by product, the underlying lattice theory by F. Kammueller has been extended.

Subject Keywords

Proof theory

URI

http://etd.lib.metu.edu.tr/upload/1097757/index.pdf
https://hdl.handle.net/11511/13615

Collections

Graduate School of Natural and Applied Sciences, Thesis

Suggestions

OpenMETU
Core

Application of the theory of constraints to an elective course registration system Üstün, Pınar; Onay, Lamia Zeynep; Department of Business Administration (2010) The Theory of Constraints (TOC) is a holistic management philosophy put forward by Eliyahu Goldratt in 1984. The thinking process and improvement tools discussed in this theory are mainly geared to manufacturing environments, however their applicability to service environments has also been shown for private professional service organizations. This study demonstrates that the steps and principles of the TOC can also be applied to non-profit services, such as the elective course registration process describe...
Quantum system structures of quantum spaces and entanglement breaking maps Dosi, A. A. (IOP Publishing, 2019-07-01) This paper is devoted to the classification of quantum systems among the quantum spaces. In the normed case we obtain a complete solution to the problem when an operator space turns out to be an operator system. The min and max quantizations of a local order are described in terms of the min and max envelopes of the related state spaces. Finally, we characterize min-max-completely positive maps between Archimedean order unit spaces and investigate entanglement breaking maps in the general setting of quantum...
Exact solutions of the modified Kratzer potential plus ring-shaped potential in the d-dimensional Schrodinger equation by the Nikiforov-Uvarov method IKHDAİR, SAMEER; Sever, Ramazan (World Scientific Pub Co Pte Lt, 2008-02-01) We present analytically the exact energy bound-states solutions of the Schrodinger equation in D dimensions for a recently proposed modified Kratzer plus ring-shaped potential by means of the Nikiforov-Uvarov method. We obtain an explicit solution of the wave functions in terms of hyper-geometric functions (Laguerre polynomials). The results obtained in this work are more general and true for any dimension which can be reduced to the well-known three-dimensional forms given by other works.
On the smoothness of solutions of impulsive autonomous systems Akhmet, Marat (Elsevier BV, 2005-01-01) The aim of this paper is to investigate dependence of solutions on parameters for nonlinear autonomous impulsive differential equations. We will specify what continuous, differentiable and analytic dependence of solutions on parameters is, define higher order derivatives of solutions with respect to parameters and determine conditions for existence of such derivatives. The theorem of analytic dependence of solutions on parameters is proved.
A SPINOR MODEL FOR QUANTUM COSMOLOGY DERELI, T; ONDER, M; TUCKER, RW (1994-03-31) The question of the interpretation of Wheeler-DeWitt solutions in the context of cosmological models is addressed by implementing the Hamiltonian constraint as a spinor wave equation in minisuperspace. We offer a relative probability interpretation based on a non-closed vector current in this space and a prescription for a parametrisation of classical solutions in terms of classical time. Such a prescription can accommodate classically degenerate metrics describing manifolds with signature change. The relat...

Citation Formats

B. Sertkaya, “Proof of the basic theorem on concept lattices in Isabelle/HOL,” M.S. - Master of Science, Middle East Technical University, 2003.