Zobrazeno 1 - 10
of 225
pro vyhledávání: '"Ghilardi, Silvio"'
We develop a method to recognize admissibility of $\Pi_{2}$-rules, relating this problem to a specific instance of the unification problem with linear constants restriction, called here "unification with simple variable restriction". It is shown that
Externí odkaz:
http://arxiv.org/abs/2406.03265
The symmetric strict implication calculus $\mathsf{S^2IC}$, introduced in [5], is a modal calculus for compact Hausdorff spaces. This is established through de Vries duality, linking compact Hausdorff spaces with de Vries algebras-complete Boolean al
Externí odkaz:
http://arxiv.org/abs/2402.00528
Taking inspiration from the monadicity of complete atomic Boolean algebras, we prove that profinite modal algebras are monadic over Set. While analyzing the monadic functor, we recover the universal model construction - a construction widely used in
Externí odkaz:
http://arxiv.org/abs/2305.04592
Modeling and verification of dynamic systems operating over a relational representation of states are increasingly investigated problems in AI, Business Process Management, and Database Theory. To make these systems amenable to verification, the amou
Externí odkaz:
http://arxiv.org/abs/2208.06377
Interpolation is an essential tool in software verification, where first-order theories are used to constrain datatypes manipulated by programs. In this paper, we introduce the datatype theory of contiguous arrays with maxdiff, where arrays are compl
Externí odkaz:
http://arxiv.org/abs/2204.11771
We devise three strategies for recognizing admissibility of non-standard inference rules via interpolation, uniform interpolation, and model completions. We apply our machinery to the case of symmetric implication calculus $\mathsf{S^2IC}$, where we
Externí odkaz:
http://arxiv.org/abs/2201.06076
Publikováno v:
In Annals of Pure and Applied Logic July 2024 175(7)
Most of the research on temporalized Description Logics (DLs) has concentrated on the case where temporal operators can occur within DL concept descriptions. In this setting, reasoning usually becomes quite hard if rigid roles, i.e., roles whose inte
Externí odkaz:
https://tud.qucosa.de/id/qucosa%3A79501
https://tud.qucosa.de/api/qucosa%3A79501/attachment/ATT-0/
https://tud.qucosa.de/api/qucosa%3A79501/attachment/ATT-0/
Autor:
Baader, Franz, Ghilardi, Silvio
Basically, the connection of two many-sorted theories is obtained by taking their disjoint union, and then connecting the two parts through connection functions that must behave like homomorphisms on the shared signature. We determine conditions unde
Externí odkaz:
https://tud.qucosa.de/id/qucosa%3A79330
https://tud.qucosa.de/api/qucosa%3A79330/attachment/ATT-0/
https://tud.qucosa.de/api/qucosa%3A79330/attachment/ATT-0/
In this paper, the theory of McCarthy's extensional arrays enriched with a maxdiff operation (this operation returns the biggest index where two given arrays differ) is proposed. It is known from the literature that a diff operation is required for t
Externí odkaz:
http://arxiv.org/abs/2010.07082