Related papers: Query Answering in Lattice-based Description Logic
A detailed exposition of foundations of a logic-algebraic model for reasoning with knowledge bases specified by propositional (Boolean) logic is presented. The model is conceived from the logical translation of usual derivatives on…
Dependent type theory gives an expressive type system facilitating succinct formalizations of mathematical concepts. In practice, it is mainly used for interactive theorem proving with intensional type theories, with PVS being a notable…
This paper seeks to apply categorical logic to the design of artificial intelligent agents that reason symbolically about objects more richly structured than sets. Using Johnstone's sequent calculus of terms- and formulae-in-context, we…
In this paper we present analytic tableau proof systems for various justification logics. We show that the tableau systems are sound and complete with respect to Mkrtychev models. In order to prove the completeness of the tableaux, we give…
We study the problem of finite entailment of ontology-mediated queries. Going beyond local queries, we allow transitive closure over roles. We focus on ontologies formulated in the description logics ALCOI and ALCOQ, extended with…
This paper studies Linear Temporal Logic over Finite Traces (LTLf) where proposition letters are replaced with first-order formulas interpreted over arbitrary theories, in the spirit of Satisfiability Modulo Theories. The resulting logic,…
We propose a novel framework to facilitate the on-demand design of data-centric systems by exploiting domain knowledge from an existing ontology. Its key ingredient is a process that we call focusing, which allows to obtain a schema for a…
Query Understanding is a semantic search method that can classify tokens in a customer's search query to entities such as Product, Brand, etc. This method can overcome the limitations of bag-of-words methods but requires an ontology. We…
We prove "untyping" theorems: in some typed theories (semirings, Kleene algebras, residuated lattices, involutive residuated lattices), typed equations can be derived from the underlying untyped equations. As a consequence, the…
We introduce ontology-mediated planning, in which planning problems are combined with an ontology. Our formalism differs from existing ones in that we focus on a strong separation of the formalisms for describing planning problems and…
The following contribution introduces a concept that employs Large Language Models (LLMs) and a chatbot interface to enhance SPARQL query generation for ontologies, thereby facilitating intuitive access to formalized knowledge. Utilizing…
We present the architecture and the evaluation of a new system for recognizing textual entailment (RTE). In RTE we want to identify automatically the type of a logical relation between two input texts. In particular, we are interested in…
Treating syntactic equality as a logical connective -- governed by left- and right-introduction rules within the sequent calculus -- offers an elegant and powerful approach to term identity. This treatment of equality allows for the…
In this article we introduce theory and algorithms for learning discrete representations that take on a lattice that is embedded in an Euclidean space. Lattice representations possess an interesting combination of properties: a) they can be…
We investigate the problem whether two ALC ontologies are indistinguishable (or inseparable) by means of queries in a given signature, which is fundamental for ontology engineering tasks such as ontology versioning, modularisation, update,…
We study privacy-preserving query answering in Description Logics (DLs). Specifically, we consider the approach of controlled query evaluation (CQE) based on the notion of instance indistinguishability. We derive data complexity results for…
We develop an incremental tableau-based decision procedures for the Alternating-time temporal logic ATL and some of its variants. While running within the theoretically established complexity upper bound, we claim that our tableau is…
Ontologies are known to improve the accuracy of Large Language Models (LLMs) when translating natural language queries into a formal query language like SQL or SPARQL. There are two ways to leverage ontologies when working with LLMs. One is…
The ability to summarize and organize knowledge into abstract concepts is key to learning and reasoning. Many industrial applications rely on the consistent and systematic use of concepts, especially when dealing with decision-critical…
Recent works have explored the use of counting queries coupled with Description Logic ontologies. The answer to such a query in a model of a knowledge base is either an integer or $\infty$, and its spectrum is the set of its answers over…