scholarly journals Logical Separability of Incomplete Data under Ontologies

2020 ◽  
Author(s):  
Jean Christoph Jung ◽  
Carsten Lutz ◽  
Hadrien Pulcini ◽  
Frank Wolter
Keyword(s):  
Incomplete Data ◽  
Decision Problem ◽  
Description Logic ◽  
Order Logic ◽  
First Order Logic ◽  
Logical Formula ◽  
Database Queries ◽  
First Order ◽  
Ontology Language ◽  
Guarded Fragment

Finding a logical formula that separates positive and negative examples given in the form of labeled data items is fundamental in applications such as concept learning, reverse engineering of database queries, and generating referring expressions. In this paper, we investigate the existence of a separating formula for incomplete data in the presence of an ontology. Both for the ontology language and the separation language, we concentrate on first-order logic and three important fragments thereof: the description logic ALCI, the guarded fragment, and the two-variable fragment. We consider several forms of separability that differ in the treatment of negative examples and in whether or not they admit the use of additional helper symbols to achieve separation. We characterize separability in a model-theoretic way, compare the separating power of the different languages, and determine the computational complexity of separability as a decision problem.

scholarly journals Ontology-Mediated Querying with the Description Logic EL: Trichotomy and Linear Datalog Rewritability

2017 ◽  
Author(s):  
Carsten Lutz ◽  
Leif Sabellek
Keyword(s):  
Description Logic ◽  
Order Logic ◽  
First Order Logic ◽  
Data Complexity ◽  
First Order ◽  
Fine Grained ◽  
Linear Recursion

We consider ontology-mediated queries (OMQs) based on an EL ontology and an atomic query (AQ), provide an ultimately fine-grained analysis of data complexity and study rewritability into linear Datalog-aiming to capture linear recursion in SQL. Our main results are that every such OMQ is in AC0, NL-complete or PTime-complete, and that containment in NL coincides with rewritability into linear Datalog (whereas containment in AC0 coincides with rewritability into first-order logic). We establish natural characterizations of the three cases, show that deciding linear Datalog rewritability (as well as the mentioned complexities) is ExpTime-complete, give a way to construct linear Datalog rewritings when they exist, and prove that there is no constant bound on the arity of IDB relations in linear Datalog rewritings.

Church’s theorem and the decision problem

2018 ◽  
Author(s):  
Rohit Parikh
Keyword(s):  
Decision Problem ◽  
Combinatorial Problem ◽  
Order Logic ◽  
First Order Logic ◽  
Negative Solution ◽  
Great Contribution ◽  
Solvable Problem ◽  
First Order ◽  
Mathematical Definition ◽  
Definition Of

Church’s theorem, published in 1936, states that the set of valid formulas of first-order logic is not effectively decidable: there is no method or algorithm for deciding which formulas of first-order logic are valid. Church’s paper exhibited an undecidable combinatorial problem P and showed that P was representable in first-order logic. If first-order logic were decidable, P would also be decidable. Since P is undecidable, first-order logic must also be undecidable. Church’s theorem is a negative solution to the decision problem (Entscheidungsproblem), the problem of finding a method for deciding whether a given formula of first-order logic is valid, or satisfiable, or neither. The great contribution of Church (and, independently, Turing) was not merely to prove that there is no method but also to propose a mathematical definition of the notion of ‘effectively solvable problem’, that is, a problem solvable by means of a method or algorithm.

Logics for the Semantic Web

2011 ◽  
pp. 24-43
Author(s):  
J. Bruijn
Keyword(s):  
Semantic Web ◽  
Logic Programming ◽  
Description Logic ◽  
Description Logics ◽  
Order Logic ◽  
First Order Logic ◽  
Horn Logic ◽  
First Order ◽  
Logical Language ◽  
Rule Languages

This chapter introduces a number of formal logical languages which form the backbone of the Semantic Web. They are used for the representation of both ontologies and rules. The basis for all languages presented in this chapter is the classical first-order logic. Description logics is a family of languages which represent subsets of first-order logic. Expressive description logic languages form the basis for popular ontology languages on the Semantic Web. Logic programming is based on a subset of first-order logic, namely Horn logic, but uses a slightly different semantics and can be extended with non-monotonic negation. Many Semantic Web reasoners are based on logic programming principles and rule languages for the Semantic Web based on logic programming are an ongoing discussion. Frame Logic allows object-oriented style (frame-based) modeling in a logical language. RuleML is an XML-based syntax consisting of different sublanguages for the exchange of specifications in different logical languages over the Web.

scholarly journals Undecidable relativizations of algebras of relations

1999 ◽  
Vol 64 (2) ◽  
pp. 747-760 ◽  
Author(s):  
Szabolcs Mikulás ◽  
Maarten Marx
Keyword(s):  
Order Logic ◽  
First Order Logic ◽  
Similarity Type ◽  
First Order ◽  
Equational Theories ◽  
Algebras Of Relations ◽  
Guarded Fragment ◽  
Cylindric Set Algebras

AbstractIn this paper we show that relativized versions of relation set algebras and cylindric set algebras have undecidable equational theories if we include coordinatewise versions of the counting operations into the similarity type. We apply these results to the guarded fragment of first-order logic.

scholarly journals The Triguarded Fragment with Transitivity

10.29007/z359 ◽  
2020 ◽  
Author(s):  
Emanuel Kieronski ◽  
Adam Malinowski
Keyword(s):  
Decision Procedure ◽  
Order Logic ◽  
First Order Logic ◽  
Satisfiability Problem ◽  
First Order ◽  
Free Variables ◽  
Guarded Fragment

The triguarded fragment of first-order logic is an extension of the guarded fragment in which quantification for subformulas with at most two free variables need not be guarded. Thus, it unifies two prominent decidable logics: the guarded fragment and the two-variable fragment. Its satisfiability problem is known to be undecidable in the presence of equality, but becomes decidable when equality is forbidden. We consider an extension of the tri- guarded fragment without equality by transitive relations, allowing them to be used only as guards. We show that the satisfiability problem for the obtained formalism is decidable and 2-ExpTime-complete, that is, it is of the same complexity as for the analogous exten- sion of the classical guarded fragment. In fact, in our satisfiability test we use a decision procedure for the latter as a subroutine. We also show how our approach, consisting in exploiting some existing results on guarded logics, can be used to reprove some known facts, as well as to derive some other new results on triguarded logics.

Interpolation for extended modal languages

2005 ◽  
Vol 70 (1) ◽  
pp. 223-234 ◽  
Author(s):  
Balder ten Cate
Keyword(s):  
Difference Operator ◽  
Relation Algebra ◽  
Order Logic ◽  
Hybrid Logic ◽  
First Order Logic ◽  
Modal Language ◽  
First Order ◽  
Language L ◽  
Guarded Fragment

AbstractSeveral extensions of the basic modal language are characterized in terms of interpolation. Our main results are of the following form: Language L′ is the least expressive extension of L with interpolation. For instance, let ℳ(D) be the extension of the basic modal language with a difference operator [7], First-order logic is the least expressive extension of ℳ(D) with interpolation. These characterizations are subsequently used to derive new results about hybrid logic, relation algebra and the guarded fragment.

scholarly journals Using formal ontology for the representation of morphological properties of anatomical structures in endoscopic surgery

2020 ◽  
Vol 6 (1) ◽  
Author(s):  
Ralph Schäfermeier ◽  
Alexandr Uciteli ◽  
Stefan Kropf ◽  
Heinrich Herre
Keyword(s):  
Endoscopic Surgery ◽  
Description Logic ◽  
Order Logic ◽  
First Order Logic ◽  
Morphological Properties ◽  
Formal Ontology ◽  
Anatomical Structures ◽  
Landmark Recognition ◽  
First Order ◽  
Formal Framework

AbstractIn this paper we present results to the problem of an adequate and compact symbolic representation of morphological features of anatomical structures that serve as surgical landmarks for automated assistance in endoscopic surgery using the General Formal Ontology (GFO) as a formal framework. For this purpose, we employed a translation from this first-order logic representation to a more compact description logic based formalism with the associated benefits, such as the availability of decidable reasoning procedures, for the purpose of automated landmark recognition in a hybrid symbolic/subsymbolic AI approach.

scholarly journals A Characterization Theorem for a Modal Description Logic

2017 ◽  
Author(s):  
Paul Wild ◽  
Lutz Schröder
Keyword(s):  
Description Logic ◽  
Description Logics ◽  
Characterization Theorem ◽  
Expressive Power ◽  
Order Logic ◽  
First Order Logic ◽  
Standard Description ◽  
First Order ◽  
Information State ◽  
Modal Description

Modal description logics feature modalities that capture dependence of knowledge on parameters such as time, place, or the information state of agents. E.g., the logic S5-ALC combines the standard description logic ALC with an S5-modality that can be understood as an epistemic operator or as representing (undirected) change. This logic embeds into a corresponding modal first-order logic S5-FOL. We prove a modal characterization theorem for this embedding, in analogy to results by van Benthem and Rosen relating ALC to standard first-order logic: We show that S5-ALC with only local roles is, both over finite and over unrestricted models, precisely the bisimulation-invariant fragment of S5-FOL, thus giving an exact description of the expressive power of S5-ALC with only local roles.

scholarly journals The Triguarded Fragment of First-Order Logic

10.29007/m8ts ◽  
2018 ◽  
Author(s):  
Sebastian Rudolph ◽  
Mantas Simkus
Keyword(s):  
Description Logics ◽  
Past Research ◽  
Order Logic ◽  
First Order Logic ◽  
Crucial Importance ◽  
Natural Assumption ◽  
First Order ◽  
Natural Extensions ◽  
Guarded Fragment ◽  
Definition Of

Past research into decidable fragments of first-order logic (FO) has produced two very prominent fragments: the guarded fragment GF, and the two-variable fragment FO2. These fragments are of crucial importance because they provide significant insights into decidabil- ity and expressiveness of other (computational) logics like Modal Logics (MLs) and various Description Logics (DLs), which play a central role in Verification, Knowledge Represen- tation, and other areas. In this paper, we take a closer look at GF and FO2, and present a new fragment that subsumes them both. This fragment, called the triguarded fragment (denoted TGF), is obtained by relaxing the standard definition of GF: quantification is required to be guarded only for subformulae with three or more free variables. We show that, in the absence of equality, satisfiability in TGF is N2ExpTime-complete, but becomes NExpTime-complete if we bound the arity of predicates by a constant (a natural assumption in the context of MLs and DLs). Finally, we observe that many natural extensions of TGF, including the addition of equality, lead to undecidability.

Sign in / Sign up

Export Citation Format

Share Document