zbMATH — the first resource for mathematics

Mechanised assessment of complex natural-language arguments using expressive logic combinations. (English) Zbl 1435.68315
Herzig, Andreas (ed.) et al., Frontiers of combining systems. 12th international symposium, FroCoS 2019, London, UK, September 4–6, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11715, 112-128 (2019).
Summary: We present and illustrate an approach to combining logics based on shallow semantical embeddings, a technique that harnesses the high expressive power of classical higher-order logic (HOL) as a meta-language in order to embed the syntax and semantics of some object logic. This approach allows us to reuse existing (higher-order) automated reasoning infrastructure for seamlessly combining and reasoning with different non-classical logics (modal, deontic, intensional, epistemic, etc.). In particular, the work presented here illustrates the utilisation of the Isabelle proof assistant for the representation and assessment of linguistically complex arguments. We illustratively combine a dyadic deontic logic (also featuring alethic modalities) enhanced with higher-order quantifiers and a 2D-semantics drawing on Kaplan’s logic of indexicals.
For the entire collection see [Zbl 1428.68022].

68T27 Logic in artificial intelligence
68T50 Natural language processing
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Isabelle; Nitpick
Full Text: DOI