Disjunction and Modular Proof Search

Title: Disjunction and Modular Proof Search

Research Question: Can the modularity and locality of assumptions be enforced during goal-directed proof search in first-order multi-modal logics?

Methodology: The study explores the proof-theoretic interaction between logical inferences and information flow in first-order multi-modal logics. It presents two equivalent ways of formulating modal inference, which enforces a discipline of structural scope in proofs. This allows for the description of modular and local reasoning, where only specific program statements can contribute to the proof of a goal.

Results: The research demonstrates that it is possible to enforce modularity and locality during goal-directed proof search. It shows that inferences can be applied in any order, while still maintaining the characteristic modular information flow. This result has implications for the design of proof systems and the development of knowledge representation systems.

Implications: The findings of this study have implications for the design of proof systems and the development of knowledge representation systems. It suggests that the modularity and locality of assumptions can be enforced during goal-directed proof search, which can lead to more efficient and accurate reasoning tasks. This research also contributes to the broader understanding of expressive modality in practical knowledge representation.

Link to Article: https://arxiv.org/abs/0104021v2 Authors: arXiv ID: 0104021v2