Modularity and relevant logic (Q584243)

This paper addresses the theoretical problem of practical reasoning systems (natural and artificial) being both correct and efficient. The problem of guaranteeing both has engendered disillusionment with formal logic in the AI community [see \textit{C. Cherniak}, J. Philos. 81, 739-758 (1984), for instance]. However, the abandonment of formal logic for the sake of efficiency has led to more or less ad hoc techniques, e.g., specific-context-bound semantic nets, frames, etc., which are not known to be correct. This paper explores a model in which reasoning systems consist of an assembly of \underbar{logical} modules (each one meets the conditions of local consistency and completeness) using procedural derivations in a relevant logic, and shows that having a combination of both speed and logical accuracy is at last an open possibility. For different discussions and approaches to this issue which include using relevant logics, see \textit{P. B. Thistlewaite}, \textit{M. A. McRobbie} and \textit{R. K. Meyer} [Automatic theorem proving in non-classical logics (John Wiley and Sons, Inc.) (1988)] and \textit{N. D. Belnap} jun. [``How a computer should think'', in: Contemporary aspects of philosophy (\textit{G. Ryle} (ed.)), 30-55 (Oriel Press) (1988), and ``A useful four-valued logic'' in: Modern uses of multiple valued logic, 5-37 (1978; Zbl 0424.03012)]. A reasoner is to have a global logic G, and is to consist of a set of modules and a selector, where a module consists of i) a set of rules that define the set of sentences that comprises its domain of expertise, ii) a set of inference rules and iii) a set of sentences that serve as its data. The global data is the data in all of the modules, and the global domain is the union of domains of all the modules. The selector assigns a module to each sentence in the global domain. A sentence is correct (for G) just in case it is derivable (according to G) from the global data. A sentence is provable in a module if there is a proof of it from its data using its inference rules. A module is locally consistent (for G) provided that all of its provable sentences are correct, and locally complete (for G) just in case all of the correct sentences of its domain are provable in it. A module is logical (for G) iff it is locally consistent and complete. And a sentence is provable in a reasoner iff it can be proven in the module for which it is selected. Obviously, the stipulation that all modules be logical guarantees that the reasoner can prove exactly what is correct. The author goes on to motivate such logical modules by showing that they have many properties appropriately analogous to the input modules of \textit{J. Fodor} [The modularity of mind (MIT Press, Cambridge, Mass.) (1983)], e.g., domain specificity, independence, etc. With respect to the choice of global logic, the author reasonably contends that classical logic will be unsuitable because the reasoner must be tolerant of inconsistency in the global data. (Since predicate logic is undecidable, there can be no reliable consistency check.) Since classical logic endorses the Ex Falsum Quod Libet, inconsistency in the global data would force each module to prove every sentence in its domain in order to be correct - even if its own restricted data is consistent. (We should note that the same is true of the normal sorts of modal logics.) The author then recommends the implication-negation fragment of QR (the quantificational extension of the system R of relevant implication, here taken to have intensional disjunction and conjunction defined in the usual manner) to be the global logic of reasoners since 1) it is suitably tolerant of inconsistency (i.e., it is weakly paraconsistent in the language of \textit{R. Routley}, \textit{V. Plumwood}, \textit{R. K. Meyer} and \textit{R. T. Brady} [Relevant logics and their rivals, Vol. 1 (1982; Zbl 0579.03011)]), and 2) it is practically efficient - indeed, procedural derivation, the method actually used for logic programming (see \textit{R. Kolwalski} [Logic for problem solving (1979; Zbl 0426.68002)]) is equivalent to it on suitable translation. The latter point is formally proven in the appendix of the paper.