2001/04/30 by Matthew Stone, Stone, Matthew
Computer Science · #Distributed systems and fault tolerance #F.4.1 #FOS: Computer and information sciences #I.2.3 #I.2.4 #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.LO
paper · pdf · doi:10.48550/arxiv.cs/0104021
openalex publication_date 2001/04/30 · arxiv created 2002/06/05 · arxiv updated 2009/11/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.