Disjunction and modular goal-directed proof search

Research output: Contribution to journalArticle


This article explores goal-directed proof search in first-order multimodal logic. I focus on a family of modal logics which offer the expressive power to specify modular goals and local assumptions. A modular goal must be proved from designated assumptions; conversely, a local assumption can only be used to prove a designated goal. Indefinite modal specifications can avoid combinatorial interactions among independent ambiguities by making separate goals modular and corresponding disjunctive alternatives local. Such specifications can effectively guarantee that provable goals have short proofs. The key result of this article is to establish a sound and complete goal-directed proof system that actively uses the modularity and locality of modal logic to constrain proof search. In particular, logically independent, local ambiguities will not interact in proof search. The challenge is that, in goal-directed proof, a modal prover cannot simply reason locally, in a module, because modularity is a property of formulas rather than proof problems. The result therefore requires prior proof-theoretic justifications of logic programming to be extended, strengthened, and combined with new proof-theoretic analyses of modal deduction.

Original languageEnglish (US)
Pages (from-to)539-577
Number of pages39
JournalACM Transactions on Computational Logic
Issue number3
StatePublished - Jul 1 2005

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)
  • Logic
  • Computational Mathematics


  • Goal-directed proof
  • Indefinite information
  • Locality
  • Logic programming
  • Modal logic
  • Modularity

Fingerprint Dive into the research topics of 'Disjunction and modular goal-directed proof search'. Together they form a unique fingerprint.

Cite this