Renate A. Schmidt

KR Conference 2020 Conference Paper

Signature-Based Abduction for Expressive Description Logics

• Patrick Koopmann
• Warren Del-Pinto
• Sophie Tourret
• Renate A. Schmidt

Signature-based abduction aims at building hypotheses over a specified set of names, the signature, that explain an observation relative to some background knowledge. This type of abduction is useful for tasks such as diagnosis, where the vocab- ulary used for observed symptoms differs from the vocabulary expected to explain those symptoms. We present the first complete method solving signature-based abduction for observations expressed in the expressive description logic ALC, which can include TBox and ABox axioms. The method is guaranteed to compute a finite and complete set of hypotheses, and is evaluated on a set of realistic knowledge bases.

AAAI Conference 2019 Conference Paper

ABox Abduction via Forgetting in ALC

• Warren Del-Pinto
• Renate A. Schmidt

Abductive reasoning generates explanatory hypotheses for new observations using prior knowledge. This paper investigates the use of forgetting, also known as uniform interpolation, to perform ABox abduction in description logic (ALC) ontologies. Non-abducibles are specified by a forgetting signature which can contain concept, but not role, symbols. The resulting hypotheses are semantically minimal and consist of a disjunction of ABox axioms. These disjuncts are each independent explanations, and are not redundant with respect to the background ontology or the other disjuncts, representing a form of hypothesis space. The observations and hypotheses handled by the method can contain both atomic or complex ALC concepts, excluding role assertions, and are not restricted to Horn clauses. Two approaches to redundancy elimination are explored in practice: full and approximate. Using a prototype implementation, experiments were performed over a corpus of real world ontologies to investigate the practicality of both approaches across several settings.

AAAI Conference 2019 Conference Paper

Tracking Logical Difference in Large-Scale Ontologies: A Forgetting-Based Approach

• Yizheng Zhao
• Ghadah Alghamdi
• Renate A. Schmidt
• Hao Feng
• Giorgos Stoilos
• Damir Juric
• Mohammad Khodadadi

This paper explores how the logical difference between two ontologies can be tracked using a forgetting-based or uniform interpolation (UI)-based approach. The idea is that rather than computing all entailments of one ontology not entailed by the other ontology, which would be computationally infeasible, only the strongest entailments not entailed in the other ontology are computed. To overcome drawbacks of existing forgetting/uniform interpolation tools we introduce a new forgetting method designed for the task of computing the logical difference between different versions of large-scale ontologies. The method is sound and terminating, and can compute uniform interpolants for ALC-ontologies as large as SNOMED CT and NCIt. Our evaluation shows that the method can achieve considerably better success rates (>90%) and provides a feasible approach to computing the logical difference in large-scale ontologies, as a case study on different versions of SNOMED CT and NCIt ontologies shows.

IJCAI Conference 2017 Conference Paper

Role Forgetting for ALCOQH(universal role)-Ontologies Using an Ackermann-Based Approach

• Yizheng Zhao
• Renate A. Schmidt

Forgetting refers to a non-standard reasoning problem concerned with eliminating concept and role symbols from description logic-based ontologies while preserving all logical consequences up to the remaining symbols. Whereas previous research has primarily focused on forgetting concept symbols, in this paper, we turn our attention to role symbol forgetting. In particular, we present a practical method for semantic role forgetting for ontologies expressible in the description logic ALCOQH(universal role), i. e. , the basic description logic ALC extended with nominals, qualified number restrictions, role inclusions and the universal role. Being based on an Ackermann approach, the method is the only approach so far for forgetting role symbols in description logics with qualified number restrictions. The method is goal-oriented and incremental. It always terminates and is sound in the sense that the forgetting solution is equivalent to the original ontology up to the forgotten symbols possibly with new concept definer symbols. Despite our method not being complete, performance results of an evaluation with a prototypical implementation have shown very good success rates on real-world ontologies.

SAT Conference 2016 Conference Paper

Lifting QBF Resolution Calculi to DQBF

• Olaf Beyersdorff
• Leroy Chew
• Renate A. Schmidt
• Martin Suda 0001

Abstract We examine existing resolution systems for quantified Boolean formulas (QBF) and answer the question which of these calculi can be lifted to the more powerful Dependency QBFs (DQBF). An interesting picture emerges: While for QBF we have the strict chain of proof systems \(\textsf {Q-Res}< \textsf {IR-calc} < \textsf {IRM-calc} \), the situation is quite different in DQBF. The obvious adaptations of Q-Res and likewise universal resolution are too weak: they are not complete. The obvious adaptation of IR-calc has the right strength: it is sound and complete. IRM-calc is too strong: it is not sound any more, and the same applies to long-distance resolution. Conceptually, we use the relation of DQBF to effectively propositional logic ( EPR ) and explain our new DQBF calculus based on IR-calc as a subsystem of first-order resolution.

LPAR Conference 2013 Conference Paper

Forgetting Concept and Role Symbols in $\mathcal{ALCH}$ -Ontologies

• Patrick Koopmann
• Renate A. Schmidt

Abstract We develop a resolution-based method for forgetting concept and role symbols in \(\mathcal{ALCH}\) ontologies, or for computing uniform interpolants in \(\mathcal{ALCH}\). Uniform interpolants use only a restricted set of symbols, while preserving logical consequences of the original ontology involving these symbols. While recent work towards practical methods for uniform interpolation in expressive description logics limits attention to forgetting concept symbols, we believe most applications would benefit from the possibility to forget both role and concept symbols. We focus on the description logic \(\mathcal{ALCH}\), which allows for the formalisation of role hierarchies. Our approach is based on a recently developed resolution-based calculus for forgetting concept symbols in \(\mathcal{ALC}\) ontologies, which we extend by redundancy elimination techniques to make it practical for larger ontologies. Experiments on \(\mathcal{ALCH}\) fragments of real life ontologies suggest that our method is applicable in a lot of real-life applications.

JELIA Conference 2012 Conference Paper

The Tableau Prover Generator MetTeL2

• Dmitry Tishkovsky
• Renate A. Schmidt
• Mohammad Khodadadi

Abstract This paper introduces METTEL2, a tableau prover generator producing J ava code from the specification of a tableau calculus for a logical language. METTEL2 is intended to provide an easy to use system for non-technical users and allow technical users to extend the generated implementations.

JELIA Conference 2008 Conference Paper

Improved Second-Order Quantifier Elimination in Modal Logic

• Renate A. Schmidt

Abstract This paper introduces improvements for second-order quantifier elimination methods based on Ackermann’s Lemma and investigates their application in modal correspondence theory. In particular, we define refined calculi and procedures for solving the problem of eliminating quantified propositional symbols from modal formulae. We prove correctness results and use the approach to compute first-order frame correspondence properties for modal axioms and modal rules. Our approach can solve two new classes of formulae which have wider scope than existing classes known to be solvable by second-order quantifier elimination methods.

JELIA Conference 2002 Conference Paper

Multi-agent Logics of Dynamic Belief and Knowledge

• Renate A. Schmidt
• Dmitry Tishkovsky

Abstract This paper proposes a family of logics for reasoning about the dynamic activities and informational attitudes, i. e. the beliefs and knowledge, of agents. The logics are based on a new formalisations and semantics of the test operator of propositional dynamic logic and a representation of actions which distinguishes abstract actions from concrete actions. The new test operator, called informational test, can be used to formalise the beliefs and knowledge of particular agents as dynamic modalities. This approach is consistent with the formalisation of the agents’ beliefs and knowledge as K(D)45 and S5 modalities. Properties concerning the preservation of informativeness, truthfulness and belief are proved for a derivative of the informational test operator. It is shown that common belief and common knowledge can be expressed in these logics. As a consequence, these logics are more expressive than propositional dynamic logic with an extra modality for belief or knowledge. However, the logics are still decidable and in 2EXPTIME. Versions of the considered logics express natural additional properties of beliefs or knowledge and interaction of beliefs or knowledge with actions. A simulation of PDL is constructed in one of these extensions.

KR Conference 2002 Conference Paper

Scientific Benchmarking with Temporal Logic Decision Procedures

• Ullrich Hustadt
• Renate A. Schmidt

LPAR Conference 2001 Conference Paper

Computational Space Efficiency and Minimal Model Generation for Guarded Formulae

• Lilia Georgieva
• Ullrich Hustadt
• Renate A. Schmidt

Abstract This paper describes a number of hyperresolution-based decision procedures for a subfragment of the guarded fragment. We first present a polynomial space decision procedure of optimal worst-case space and time complexity for the fragment under consideration. We then consider minimal model generation procedures which construct all and only minimal Herbrand models for guarded formulae. These procedures are based on hyperresolution, (complement) splitting and either model constraint propagation or local minimality tests. All the procedures have concrete application domains and are relevant for multi-modal and description logics that can be embedded into the considered fragment.

TIME Conference 2001 Conference Paper

Reasoning about agents in the KARO framework

• Ullrich Hustadt
• Clare Dixon
• Renate A. Schmidt
• Michael Fisher 0001
• John-Jules Ch. Meyer
• Wiebe van der Hoek

This paper proposes two methods for realising automated reasoning about agent-based systems. The framework for modelling intelligent agent behaviour that we focus on is a core of KARO logic, an expressive combination of various modal logics including propositional dynamic logic, a modal logic of knowledge, a modal logic of wishes, and additional non-standard operators. The first method we present is based on a translation of core KARO logic to first-order logic combined with first-order resolution. The second method uses an embedding of core KARO logic into a combination of branching-time temporal logic CTL and multi-modal S5 plus a clausal resolution calculus for these combined logics. We discuss the advantages and shortcomings of each approach and suggest ways to extend each variant to cover more of the KARO framework.

IJCAI Conference 1997 Conference Paper

On evaluating decision procedures for modal logic

• Ullrich Hustadt
• Renate A. Schmidt

This paper investigates the evaluation method of decision procedures for multi-modal logic proposed by Giunchiglia and Sebastiani as an adaptation from the evaluation method of Mitchell et al of decision procedures for propositional logic. We compare three dif­ ferent theorem proving approaches, namely the Davis-Putnam-based procedure KSAT, the tableaux-based system KTUS and a transla­ tion approach combined with first-order resolu­ tion. Our results do not support the claims of Giunchiglia and Sebastiani concerning the com­ putational superiority of KSAT over KRIS, and an easy-hard-easy pattern for randomly gener­ ated modal formulae.