Formal Concept Analysis and Resolution in Algebraic Domains
Pascal Hitzler, Matthias Wendt
备注：
14 pages. We have rewritten the old version according to the suggestions of some referees. The results are the same. The presentation is completely different
We relate two formerly independent areas: Formal concept analysis and logic of domains. We will establish a correspondene between contextual attribute logic on formal contexts resp. concept lattices and a clausal logic on coherent algebraic cpos. We show how to identify the notion of formal concept in the domain theoretic setting. In particular, we show that a special instance of the resolution rule from the domain logic coincides with the concept closure operator from formal concept analysis. The results shed light on the use of contexts and domains for knowledge representation and reasoning purposes.
Systematics Information Services, Inc.（系统信息服务公司）；University of Arkansas at Little Rock（阿肯色大学小石城分校）
This paper unites two problem-solving traditions in computer science: (1) constraint-based reasoning, and (2) formal concept analysis. For basic definitions and properties of networks of constraints, we follow the foundational approach of Montanari and Rossi. This paper advocates distributed relations as a more semantic version of networks of constraints. The theory developed here uses the theory of formal concept analysis, pioneered by Rudolf Wille and his colleagues, as a key for unlocking the hidden semantic structure within distributed relations. Conversely, this paper offers distributed r…
We discuss a formal framework for using algebraic structures to model a meta-language that can write, compose, and provide interoperability between abstractions of DSLs. The purpose of this formal framework is to provide a verification of compositional properties of the meta-language. Throughout our paper we discuss the construction of this formal framework, as well its relation to our team's work on the DARPA V-SPELLS program via the pipeline we have developed for completing our verification tasking on V-SPELLS. We aim to give a broad overview of this verification pipeline in our paper. The p…
In this paper we propose an algebraic formalization of connectors in the quantitative setting, in order to address their non-functional features in architectures of component-based systems. We firstly present a weighted Algebra of Interactions over a set of ports and a commutative and idempotent semiring, which is proved sufficient for modeling well-known coordination schemes in the weighted setup. In turn, we study a weighted Algebra of Connectors over a set of ports and a commutative and idempotent semiring, which extends the weighted Algebra of Interactions with types that encode Rendezvous…
German University in Cairo（开罗德国大学）；Cairo University（开罗大学）
Tremendous research effort has been dedicated over the years to thoroughly investigate non-monotonic reasoning. With the abundance of non-monotonic logical formalisms, a unified theory that enables comparing the different approaches is much called for. In this paper, we present an algebraic graded logic we refer to as LogAG capable of encompassing a wide variety of non-monotonic formalisms. We build on Lin and Shoham's argument systems first developed to formalize non-monotonic commonsense reasoning. We show how to encode argument systems as LogAG theories, and prove that LogAG captures the no…
We investigate monoidal categories of formal contexts, in which states correspond to formal concepts. In particular we examine the category of bonds or Chu correspondences between contexts, which is known to be equivalent to the *-autonomous category of complete sup-lattices. We show that a second monoidal structure exists on both categories, corresponding to the direct product of formal contexts defined by Ganter and Wille, and discuss the use of these categories as compositional models of meaning.
Formal Concept Analysis has proven to be an effective method of restructuring complete lattices and various algebraic domains. In this paper, the notions of attribute continuous formal context and continuous formal concept are introduced by considering a selection F of fnite subsets of attributes. Our decision of a selection F relies on a kind of generalized interior operators. It is shown that the set of continuous formal concepts forms a continuous domain, and every continuous domain can be obtained in this way. Moreover, an notion of F-morphism is also identified to produce a category equiv…
The field of $p$-adic numbers $\mathbb{Q}_p$ and the ring of $p$-adic integers $\mathbb{Z}_p$ are essential constructions of modern number theory. Hensel's lemma, described by Gouvêa as the "most important algebraic property of the $p$-adic numbers," shows the existence of roots of polynomials over $\mathbb{Z}_p$ provided an initial seed point. The theorem can be proved for the $p$-adics with significantly weaker hypotheses than for general rings. We construct $\mathbb{Q}_p$ and $\mathbb{Z}_p$ in the Lean proof assistant, with various associated algebraic properties, and formally prove a stron…
The present paper proposes a novel way to unify Rough Set Theory and Formal Concept Analysis. Our method stems from results and insights developed in the algebraic theory of modal logic, and is based on the idea that Pawlak's original approximation spaces can be seen as special instances of enriched formal contexts, i.e. relational structures based on formal contexts from Formal Concept Analysis.
As the second part of the treatise 'A General Theory of Concept Lattice', this paper speaks of the tractability of the general concept lattice for both its lattice structure and logic content. The general concept lattice permits a feasible construction that can be completed in a single scan of the formal context, though the conventional formal-concept lattice and rough-set lattice can be regained from the general concept lattice. The logic implication deducible from the general concept lattice takes the form of μ_1 {\rightarrow} μ_2 where μ_1,μ_2 {\in} M^{\ast} are composite attributes out of …
The purpose of this paper is to explore the question "to what extent could we produce formal, machine-verifiable, proofs in real algebraic geometry?" The question has been asked before but as yet the leading algorithms for answering such questions have not been formalised. We present a thesis that a new algorithm for ascertaining satisfiability of formulae over the reals via Cylindrical Algebraic Coverings [Ábrahám, Davenport, England, Kremer, \emph{Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driver Search Using Cylindrical Algebraic Coverings}, 2020] mig…
It is known that a (concept) lattice contains an n-dimensional Boolean suborder if and only if the context contains an n-dimensional contra-nominal scale as subcontext. In this work, we investigate more closely the interplay between the Boolean subcontexts of a given finite context and the Boolean suborders of its concept lattice. To this end, we define mappings from the set of subcontexts of a context to the set of suborders of its concept lattice and vice versa and study their structural properties. In addition, we introduce closed-subcontexts as an extension of closed relations to investiga…
