ABSTRACT. Forgetting enables users to create compact views of knowledge bases of logical formulas over a user-specified signature by performing inferences on the symbols outside this signature. These views are easier to navigate, analyse and query, and are reusable as stand-alone knowledge bases in other settings. In this presentation I will give an overview of our work on the development and application of forgetting methods for description and modal logics. After an introduction to the idea of forgetting and the two forms of forgetting (deductive and semantic forgetting), I will discuss current advances and challenges in automating and applying forgetting.

ABSTRACT. We present a Coq formalization of the Quantified Reflection Calculus with one modality, or QRC1. This is a decidable, strictly positive, and quantified modal logic previously studied for its applications in proof theory. The highlights are a deep embedding of QRC1 in the Coq proof assistant, a mechanization of the notion of Kripke model with varying domains and a formalization of the soundness theorem. We focus on the design decisions inherent to the formalization and the insights that led to new and simplified proofs.

ABSTRACT. Non-normal modal logics, interpreted on neighbourhood models which generalise the usual relational semantics, have found application in several areas, such as epistemic, deontic, and coalitional reasoning. We present here preliminary results on reasoning in a family of modal description logics obtained by combining ALC with non-normal modal operators. First, we provide a framework of terminating, correct, and complete tableau algorithms to check satisfiability of formulas in such logics with the semantics based on varying domains. We then investigate the satisfiability problems in fragments of these languages obtained by restricting the application of modal operators to formulas only, and interpreted on models with constant domains, providing tight complexity results.

ABSTRACT. Anderson's emendation of Gödel's ontological proof is known as a variant that does not entail modal collapse, that is, derivability of $\nec A\leftrightarrow A$ for all formulas $A$. This variant of the axiomatization is here investigated as a case study of intuitionistic derivability using a natural deduction. The system for higher-order modal logic simulates a varying domain semantics on the object level, in a manner that seems to have been intended by Anderson. As will be shown, intuitionistic derivability is limited to conditional statements where $G(x)$ is assumed, whereas the derivability of $ G(x)$ itself is proved to be impossible. The required classical proof of $\pos \exists x. G(x)$, can be compared to the compatibility argument of Scott's version, who used a form of indirect proof.

ABSTRACT. Laws must be understood and their application must be explained and justified. As such, they seem to be the perfect use case for (non-classical) automated reasoning. Indeed, there is much academic research in legal knowledge representation and reasoning. Nevertheless, there are no commercial reasoning-based applications, apart from legal expert systems.In this talk, I will survey a personal three years journey towards a commercial application, as well as lessons learned from failures. I will touch various topics, such as knowledge representation and validation, reasoning and justification, and academic vs business perspectives.

ABSTRACT. We investigate the simplification of parameterised Boolean equation systems (PBESs), a first-order fixpoint logic, by means of quantifier manipulation. Whereas the occurrence of quantifiers in a PBES can significantly increase the effort required to solve a PBES, i.e., compute its semantics, existing syntactic transformations have little to no support for quantifiers. We resolve this, by proposing a static analysis algorithm that identifies which quantifiers may be moved between equations such that their scope is reduced. This syntactic transformation can drastically reduce the effort required to solve a PBES. Additionally, we identify an improvement to the computation of guards, which can be used to strengthen our static analysis.

ABSTRACT. Prefixes and an additional prefix unification can be used when performing proof search in some popular non-classical logics. The paper presents two techniques that optimize this approach for the first-order modal logics D and S5. The paper describes implementations of both techniques and presents a practical evaluation that shows the resulting performance improvement.

ABSTRACT. We report our first results regarding the automated verification of deontic correspondences (and related matters) in Isabelle/HOL, analogous to what has been achieved for the modal logic cube.

ABSTRACT. This paper describes an evaluation of ATP systems on the QMLTP library of first-order modal logic problems. Principally, the problems are translated to higher-order logic in the TPTP languages using an embedding approach, and solved using higher-order logic ATP systems. Additionally, the results from native modal logic ATP systems are considered, and compared with those from the embedding approach. The conclusions are that (i) The embedding process is reliable and successful. (ii) The choice of backend ATP system can significantly impact the performance of the embedding approach. (iii) Native modal logic ATP systems outperform the embedding approach over the QMLTP problems. (iv) The embedding approach can cope with a wider range modal logics than the native modal systems considered.