Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userConverting ALC Connection Proofs into ALC Sequents
100
0
0.0
(
0
)
Added by
EPTCS
Publication date
2019
fields
Informatics Engineering
and research's language is
English
Authors
Eunice Palmeira
Ask ChatGPT about the research
No Arabic abstract
The connection method has earned good reputation in the area of automated theorem proving, due to its simplicity, efficiency and rational use of memory. This method has been applied recently in automatic provers that reason over ontologies written in the description logic ALC. However, proofs generated by connection calculi are difficult to understand. Proof readability is largely lost by the transformations to disjunctive normal form applied over the formulae to be proven. Such a proof model, albeit efficient, prevents inference systems based on it from effectively providing justifications and/or descriptions of the steps used in inferences. To address this problem, in this paper we propose a method for converting matricial proofs generated by the ALC connection method to ALC sequent proofs, which are much easier to understand, and whose translation to natural language is more straightforward. We also describe a calculus that accepts the input formula in a non-clausal ALC format, what simplifies the translation.
rate research
Read More
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, and forgetting. We consider both knowledge base (KB) and TBox inseparability. For KBs, we give model-theoretic criteria in terms of (finite partial) homomorphisms and products and prove that this problem is undecidable for conjunctive queries (CQs), but 2ExpTime-complete for unions of CQs (UCQs). The same results hold if (U)CQs are replaced by rooted (U)CQs, where every variable is connected to an answer variable. We also show that inseparability by CQs is still undecidable if one KB is given in the lightweight DL EL and if no restrictions are imposed on the signature of the CQs. We also consider the problem whether two ALC TBoxes give the same answers to any query over any ABox in a given signature and show that, for CQs, this problem is undecidable, too. We then develop model-theoretic criteria for Horn-ALC TBoxes and show using tree automata that, in contrast, inseparability becomes decidable and 2ExpTime-complete, even ExpTime-complete when restricted to (unions of) rooted CQs.
Approaches based on refinement operators have been successfully applied to class expression learning on RDF knowledge graphs. These approaches often need to explore a large number of concepts to find adequate hypotheses. This need arguably stems from current approaches relying on myopic heuristic functions to guide their search through an infinite concept space. In turn, deep reinforcement learning provides effective means to address myopia by estimating how much discounted cumulated future reward states promise. In this work, we leverage deep reinforcement learning to accelerate the learning of concepts in $mathcal{ALC}$ by proposing DRILL -- a novel class expression learning approach that uses a convolutional deep Q-learning model to steer its search. By virtue of its architecture, DRILL is able to compute the expected discounted cumulated future reward of more than $10^3$ class expressions in a second on standard hardware. We evaluate DRILL on four benchmark datasets against state-of-the-art approaches. Our results suggest that DRILL converges to goal states at least 2.7$times$ faster than state-of-the-art models on all benchmark datasets. We provide an open-source implementation of our approach, including training and evaluation scripts as well as pre-trained models.
Description Logics (DLs) are a family of languages used for the representation and reasoning on the knowledge of an application domain, in a structured and formal manner. In order to achieve this objective, several provers, such as RACER and FaCT++, have been implemented, but these provers themselves have not been yet certified. In order to ensure the soundness of derivations in these DLs, it is necessary to formally verify the deductions applied by these reasoners. Formal methods offer powerful tools for the specification and verification of proof procedures, among them there are methods for proving properties such as soundness, completeness and termination of a proof procedure. In this paper, we present the definition of a proof procedure for the Description Logic ALC, based on a semantic tableau method. We ensure validity of our prover by proving its soundness, completeness and termination properties using Isabelle proof assistant. The proof proceeds in two phases, first by establishing these properties on an abstract level, and then by instantiating them for an implementation based on lists.
Star-formation rates (SFRs) of galaxies are commonly calculated by converting the measured Halpha luminosities (L_Halpha) into current SFRs. This conversion is based on a constant initial mass function (IMF) independent of the total SFR. As recently recognised the maximum stellar mass in a star cluster is limited by the embedded total cluster mass and, in addition, the maximum embedded star cluster mass is constrained by the current SFR. The combination of these two relations leads to an integrated galaxial initial stellar mass function (IGIMF, the IMF for the whole galaxy) which is steeper in the high mass regime than the constant canonical IMF, and is dependent on the SFR of the galaxy. Consequently, the L_Halpha-SFR relation becomes non-linear and flattens for low SFRs. Especially for dwarf galaxies the SFRs can be underestimated by up to three orders of magnitude. We revise the existing linear L_Halpha-SFR relations using our IGIMF notion. These are likely to lead to a revision of the cosmological star formation histories. We also demonstrate that in the case of the Sculptor dwarf irregular galaxies the IGIMF-formalism implies a linear dependence of the total SFR on the total galaxy gas mass. A constant gas depletion time scale of a few Gyrs results independently of the galaxy gas mass with a reduced scatter compared to the conventional results. Our findings are qualitatively independent of the explicit choice of the IGIMF details and challenges current star formation theory in dwarf galaxies.
In this work we study the cost of local and global proofs on distributed verification. In this setting the nodes of a distributed system are provided with a nondeterministic proof for the correctness of the state of the system, and the nodes need to verify this proof by looking at only their local neighborhood in the system. Previous works have studied the model where each node is given its own, possibly unique, part of the proof as input. The cost of a proof is the maximum size of an individual label. We compare this model to a model where each node has access to the same global proof, and the cost is the size of this global proof. It is easy to see that a global proof can always include all of the local proofs, and every local proof can be a copy of the global proof. We show that there exists properties that exhibit these relative proof sizes, and also properties that are somewhere in between. In addition, we introduce a new lower bound technique and use it to prove a tight lower bound on the complexity of reversing distributed decision and establish a link between communication complexity and distributed proof complexity.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
