Towards a generic theorem prover for non-classical logics
We introduce atomic and molecular logics. They are somehow 'universal'.
Indeed, every logic such that its truth conditions are expressible in
terms of first-order formulas is as expressive as an atomic or a
molecular logic. We show how automatic display and Hilbert calculi can
be defined for any atomic and molecular logics whose connectives are
so-called 'universal'. We provide examples of such automatic proof calculi
for already well-known logics such as modal logic and the Lambek calculus.
We sketch a correspondence theory for atomic logics and molecular logics
which allows us to extend the automatic generation of proof calculi to
logics whose semantics are defined by specific conditions on the class of
models. We apply these correspondence results to propositional logic and
rediscover already well-known proof calculi for it.
HOL, Universal Meta-Logical Reasoning in HOL and LogiKEy — A brief Introduction
In this talk, I will first explain some of the merits of classical higher-order logic (HOL) and give an overview of my own contributions to the field. Then, I will outline the universal meta-logical reasoning approach that I have been developing and promoting with colleagues for about 15 years to enable flexible automation of quantified non-classical logics within HOL reasoners. Finally, I will outline the multi-layered LogiKEy methodology and infrastructure that enables the exploration of knowledge representation and reasoning solutions in non-trivial application domains, where even the object logics of interest (and combinations thereof) become negotiable.
Machine-processable Norms for Autonomous Vehicles
We present our concept for formalizing norms and employing automated reasoning in autonomous driving applications. The quantity of norms in traffic is huge and to formalize norms at such scale, a domain expert will be able to use our computer-aided formalization tool that is currently under development.
Rajeev Goré (jww. Cormac Kikkert and Robert McArthur)
CEGAR-Tableaux: improved modal satisfiability via modal clause-learning and SAT
We present CEGAR-Tableaux, a tableaux-like method for propositional
modal logics utilising SAT-solvers, modal clause-learning and multiple
optimisations from modal and description logic tableaux calculi. We
use the standard Counter-example Guided Abstract Refinement (CEGAR)
strategy for SAT-solvers to mimic a tableau-like search strategy that
explores a rooted tree-model with the classical propositional logic
part of each Kripke world evaluated using a SAT-solver. Unlike modal
encodings into SAT-solvers and modal resolution methods, we do not
explicitly represent the accessibility relation but track it
implicitly via recursion. By using ``satisfiability under unit
assumptions'', we can iterate rather than ``backtrack'' over the
satisfiable diamonds at the same modal level (context) of the tree
model with one SAT-solver. By keeping modal contexts separate from one
another, we add further refinements for reflexivity and transitivity
which manipulate modal contexts once only. Our solver CEGARBox is,
overall, the best for modal logics K, KT and S4 over the standard
benchmarks, sometimes by orders of magnitude. It can now also handle
all of the 15 logics in the modal cube as well as multimodal tense
logic Kt(n) (AKA description logic ALCI). We believe that in the
future, all tableaux calculi implementations will use CEGAR-Tableaux.
New developments in conditional deontic logic
Preference-based conditional deontic logic is a de facto standard for normative reasoning.
It offers a simple solution to contrary-to-duty paradoxes and allows to represent norms with exceptions. In this talk, I bring together under one roof various weakenings of transitivity (of the betterness relation), and present axiomatisation results for them. Taking stock, I consider the general question of finding correspondences between modal axioms and properties (in the models). So far such correspondences have been established with pen and paper. I present joint work with C. Benzmueller regarding the automated verification of these correspondences in Isabelle/HOL.
Non-Classical Reasoning in the TPTP World
Non-classical logics are used in a wide spectrum of disciplines, including artificial intelligence,
computer science, mathematics, and philosophy. The de-facto standard infrastructure for
automated theorem proving, the TPTP World, currently supports only classical logics. This
paper describes the latest extension of the TPTP World, providing languages and infrastructure
for reasoning in non-classical logics. The extension integrates seamlessly with the existing
The TPTP World - Infrastructure for Automated Reasoning
The TPTP World is a well known and established infrastructure that supports research,
development, and deployment of Automated Theorem Proving (ATP) systems for classical logics.
The data, standards, and services provided by the TPTP World have made it increasingly easy to
build, test, and apply ATP technology. This talk and tutorial reviews the core features of the
TPTP World, describes key service components of the TPTP World and how to use them, and
presents some successful applications.
Taking stock of available technologies for compliance checking on first-order knowledge
This research analyses and compares some of the automated reasoners that have been used in recent
research for compliance checking. The focus is on formalizations at the first-order level.
Past literature on normative reasoning mostly focuses on the propositional level.
However, the propositional level is of little usefulness for concrete LegalTech applications,
in which compliance checking must be enforced on (large) sets of individuals.
This paper formalizes a selected use case in the considered reasoners and compares the implementations.
The comparison will highlight that lot of further research still need to be done to integrate the
benefits featured by the different reasoners into a single standardized first-order framework.
All source codes are available at https://github.com/liviorobaldo/compliancecheckers