-
Ultraproducts in abstract categorical logic
Authors:
Marc Aiguier,
Isabelle Bloch,
Romain Pascual
Abstract:
In a previous publication, we introduced an abstract logic via an abstract notion of quantifier. Drawing upon concepts from categorical logic, this abstract logic interprets formulas from context as subobjects in a specific category, e.g., Cartesian, regular, or coherent categories, Grothendieck, or elementary toposes. We proposed an entailment system formulated as a sequent calculus which we prov…
▽ More
In a previous publication, we introduced an abstract logic via an abstract notion of quantifier. Drawing upon concepts from categorical logic, this abstract logic interprets formulas from context as subobjects in a specific category, e.g., Cartesian, regular, or coherent categories, Grothendieck, or elementary toposes. We proposed an entailment system formulated as a sequent calculus which we proved complete. Building on this foundation, our current work explores model theory within abstract logic. More precisely, we generalize one of the most important and powerful classical model theory methods, namely the ultraproduct method, and show its fundamental theorem, i.e., Los's theorem. The result is shown as independently as possible of a given quantifier.
△ Less
Submitted 4 July, 2024;
originally announced July 2024.
-
Morpho-logic from a Topos Perspective: Application to symbolic AI
Authors:
Marc Aiguier,
Isabelle Bloch,
Salim Nibouche,
Ramon Pino Perez
Abstract:
Modal logics have proved useful for many reasoning tasks in symbolic artificial intelligence (AI), such as belief revision, spatial reasoning, among others. On the other hand, mathematical morphology (MM) is a theory for non-linear analysis of structures, that was widely developed and applied in image analysis. Its mathematical bases rely on algebra, complete lattices, topology. Strong links have…
▽ More
Modal logics have proved useful for many reasoning tasks in symbolic artificial intelligence (AI), such as belief revision, spatial reasoning, among others. On the other hand, mathematical morphology (MM) is a theory for non-linear analysis of structures, that was widely developed and applied in image analysis. Its mathematical bases rely on algebra, complete lattices, topology. Strong links have been established between MM and mathematical logics, mostly modal logics. In this paper, we propose to further develop and generalize this link between mathematical morphology and modal logic from a topos perspective, i.e. categorial structures generalizing space, and connecting logics, sets and topology. Furthermore, we rely on the internal language and logic of topos. We define structuring elements, dilations and erosions as morphisms. Then we introduce the notion of structuring neighborhoods, and show that the dilations and erosions based on them lead to a constructive modal logic, for which a sound and complete proof system is proposed. We then show that the modal logic thus defined (called morpho-logic here), is well adapted to define concrete and efficient operators for revision, merging, and abduction of new knowledge, or even spatial reasoning.
△ Less
Submitted 8 March, 2023;
originally announced March 2023.
-
Abstract Mathematical morphology based on structuring element: Application to morpho-logic
Authors:
Marc Aiguier,
Isabelle Bloch,
Ramon Pino-Pérez
Abstract:
A general definition of mathematical morphology has been defined within the algebraic framework of complete lattice theory. In this framework, dealing with deterministic and increasing operators, a dilation (respectively an erosion) is an operation which is distributive over supremum (respectively infimum). From this simple definition of dilation and erosion, we cannot say much about the propertie…
▽ More
A general definition of mathematical morphology has been defined within the algebraic framework of complete lattice theory. In this framework, dealing with deterministic and increasing operators, a dilation (respectively an erosion) is an operation which is distributive over supremum (respectively infimum). From this simple definition of dilation and erosion, we cannot say much about the properties of them. However, when they form an adjunction, many important properties can be derived such as monotonicity, idempotence, and extensivity or anti-extensivity of their composition, preservation of infimum and supremum, etc. Mathematical morphology has been first developed in the setting of sets, and then extended to other algebraic structures such as graphs, hypergraphs or simplicial complexes. For all these algebraic structures, erosion and dilation are usually based on structuring elements. The goal is then to match these structuring elements on given objects either to dilate or erode them. One of the advantages of defining erosion and dilation based on structuring elements is that these operations are adjoint. Based on this observation, this paper proposes to define, at the abstract level of category theory, erosion and dilation based on structuring elements. We then define the notion of morpho-category on which erosion and dilation are defined. We then show that topos and more precisely topos of presheaves are good candidates to generate morpho-categories. However, topos do not allow taking into account the notion of inclusion between substructures but rather are defined by monics up to domain isomorphism. Therefore we define the notion of morpholizable category which allows generating morpho-categories where substructures are defined along inclusion morphisms. {A direct application of this framework is to generalize modal morpho-logic to other algebraic structures than simple sets.
△ Less
Submitted 4 May, 2020;
originally announced May 2020.
-
Explanatory relations in arbitrary logics based on satisfaction systems, cutting and retraction
Authors:
Marc Aiguier,
Jamal Atif,
Isabelle Bloch,
Ramón Pino-Pérez
Abstract:
The aim of this paper is to introduce a new framework for defining abductive reasoning operators based on a notion of retraction in arbitrary logics defined as satisfaction systems. We show how this framework leads to the design of explanatory relations satisfying properties of abductive reasoning, and discuss its application to several logics. This extends previous work on propositional logics wh…
▽ More
The aim of this paper is to introduce a new framework for defining abductive reasoning operators based on a notion of retraction in arbitrary logics defined as satisfaction systems. We show how this framework leads to the design of explanatory relations satisfying properties of abductive reasoning, and discuss its application to several logics. This extends previous work on propositional logics where retraction was defined as a morphological erosion. Here weaker properties are required for retraction, leading to a larger set of suitable operators for abduction for different logics.
△ Less
Submitted 5 March, 2018;
originally announced March 2018.
-
Dual Logic Concepts based on Mathematical Morphology in Stratified Institutions: Applications to Spatial Reasoning
Authors:
Marc Aiguier,
Isabelle Bloch
Abstract:
Several logical operators are defined as dual pairs, in different types of logics. Such dual pairs of operators also occur in other algebraic theories, such as mathematical morphology. Based on this observation, this paper proposes to define, at the abstract level of institutions, a pair of abstract dual and logical operators as morphological erosion and dilation. Standard quantifiers and modaliti…
▽ More
Several logical operators are defined as dual pairs, in different types of logics. Such dual pairs of operators also occur in other algebraic theories, such as mathematical morphology. Based on this observation, this paper proposes to define, at the abstract level of institutions, a pair of abstract dual and logical operators as morphological erosion and dilation. Standard quantifiers and modalities are then derived from these two abstract logical operators. These operators are studied both on sets of states and sets of models. To cope with the lack of explicit set of states in institutions, the proposed abstract logical dual operators are defined in an extension of institutions, the stratified institutions, which take into account the notion of open sentences, the satisfaction of which is parametrized by sets of states. A hint on the potential interest of the proposed framework for spatial reasoning is also provided.
△ Less
Submitted 16 October, 2017;
originally announced October 2017.
-
A finite basis theorem for the description logic ${\cal ALC}$
Authors:
Marc Aiguier,
Jamal Atif,
Isabelle Bloch,
Céline Hudelot
Abstract:
The main result of this paper is to prove the existence of a finite basis in the description logic ${\cal ALC}$. We show that the set of General Concept Inclusions (GCIs) holding in a finite model has always a finite basis, i.e. these GCIs can be derived from finitely many of the GCIs. This result extends a previous result from Baader and Distel, which showed the existence of a finite basis for GC…
▽ More
The main result of this paper is to prove the existence of a finite basis in the description logic ${\cal ALC}$. We show that the set of General Concept Inclusions (GCIs) holding in a finite model has always a finite basis, i.e. these GCIs can be derived from finitely many of the GCIs. This result extends a previous result from Baader and Distel, which showed the existence of a finite basis for GCIs holding in a finite model but for the inexpressive description logics ${\cal EL}$ and ${\cal EL}_{gfp}$. We also provide an algorithm for computing this finite basis, and prove its correctness. As a byproduct, we extend our finite basis theorem to any finitely generated complete covariety (i.e. any class of models closed under morphism domain, coproduct and quotient, and generated from a finite set of finite models).
△ Less
Submitted 13 January, 2017; v1 submitted 26 February, 2015;
originally announced February 2015.
-
Relaxation-based revision operators in description logics
Authors:
Marc Aiguier,
Jamal Atif,
Isabelle Bloch,
Céline Hudelot
Abstract:
As ontologies and description logics (DLs) reach out to a broader audience, several reasoning services are developed in this context. Belief revision is one of them, of prime importance when knowledge is prone to change and inconsistency. In this paper we address both the generalization of the well-known AGM postulates, and the definition of concrete and well-founded revision operators in differen…
▽ More
As ontologies and description logics (DLs) reach out to a broader audience, several reasoning services are developed in this context. Belief revision is one of them, of prime importance when knowledge is prone to change and inconsistency. In this paper we address both the generalization of the well-known AGM postulates, and the definition of concrete and well-founded revision operators in different DL families. We introduce a model-theoretic version of the AGM postulates with a general definition of inconsistency, hence enlarging their scope to a wide family of non-classical logics, in particular negation-free DL families. We propose a general framework for defining revision operators based on the notion of relaxation, introduced recently for defining dissimilarity measures between DL concepts. A revision operator in this framework amounts to relax the set of models of the old belief until it reaches the sets of models of the new piece of knowledge. We demonstrate that such a relaxation-based revision operator defines a faithful assignment and satisfies the generalized AGM postulates. Another important contribution concerns the definition of several concrete relaxation operators suited to the syntax of some DLs (ALC and its fragments EL and ELU).
△ Less
Submitted 26 February, 2015;
originally announced February 2015.
-
Belief Revision, Minimal Change and Relaxation: A General Framework based on Satisfaction Systems, and Applications to Description Logics
Authors:
Marc Aiguier,
Jamal Atif,
Isabelle Bloch,
Céline Hudelot
Abstract:
Belief revision of knowledge bases represented by a set of sentences in a given logic has been extensively studied but for specific logics, mainly propositional, and also recently Horn and description logics. Here, we propose to generalize this operation from a model-theoretic point of view, by defining revision in an abstract model theory known under the name of satisfaction systems. In this fram…
▽ More
Belief revision of knowledge bases represented by a set of sentences in a given logic has been extensively studied but for specific logics, mainly propositional, and also recently Horn and description logics. Here, we propose to generalize this operation from a model-theoretic point of view, by defining revision in an abstract model theory known under the name of satisfaction systems. In this framework, we generalize to any satisfaction systems the characterization of the well known AGM postulates given by Katsuno and Mendelzon for propositional logic in terms of minimal change among interpretations. Moreover, we study how to define revision, satisfying the AGM postulates, from relaxation notions that have been first introduced in description logics to define dissimilarity measures between concepts, and the consequence of which is to relax the set of models of the old belief until it becomes consistent with the new pieces of knowledge. We show how the proposed general framework can be instantiated in different logics such as propositional, first-order, description and Horn logics. In particular for description logics, we introduce several concrete relaxation operators tailored for the description logic $\ALC{}$ and its fragments $\EL{}$ and $\ELext{}$, discuss their properties and provide some illustrative examples.
△ Less
Submitted 13 January, 2017; v1 submitted 8 February, 2015;
originally announced February 2015.