Show/Hide Menu
Hide/Show Apps
Logout
Türkçe
Türkçe
Search
Search
Login
Login
OpenMETU
OpenMETU
About
About
Open Science Policy
Open Science Policy
Open Access Guideline
Open Access Guideline
Postgraduate Thesis Guideline
Postgraduate Thesis Guideline
Communities & Collections
Communities & Collections
Help
Help
Frequently Asked Questions
Frequently Asked Questions
Guides
Guides
Thesis submission
Thesis submission
MS without thesis term project submission
MS without thesis term project submission
Publication submission with DOI
Publication submission with DOI
Publication submission
Publication submission
Supporting Information
Supporting Information
General Information
General Information
Copyright, Embargo and License
Copyright, Embargo and License
Contact us
Contact us
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
187
views
0
downloads
Cite This
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
IEEE
ACM
APA
CHICAGO
MLA
BibTeX
B. Sertkaya, “Proof of the basic theorem on concept lattices in Isabelle/HOL,” M.S. - Master of Science, Middle East Technical University, 2003.