Disjunction and modular goal-directed proof search

TL;DR

This paper develops a modular goal-directed proof search method for first-order multi-modal logic, enabling efficient reasoning with partial information by leveraging disjunctions and proof-theoretic extensions.

Contribution

It introduces a novel proof system that respects modularity and locality in modal logic, extending proof-theoretic foundations for logic programming.

Findings

Efficient proof search in modal logic with partial information

Modular disjunctions improve reasoning efficiency

Extended proof-theoretic framework supports new proof strategies

Abstract

This paper explores goal-directed proof search in first-order multi-modal logic. The key issue is to design a proof system that respects the modularity and locality of assumptions of many modal logics. By forcing ambiguities to be considered independently, modular disjunctions in particular can be used to construct efficiently executable specifications in reasoning tasks involving partial information that otherwise might require prohibitive search. To achieve this behavior requires prior proof-theoretic justifications of logic programming to be extended, strengthened, and combined with proof-theoretic analyses of modal deduction in a novel way.