Tableau Methods for Substructural Logics

Abstract

Over the last few decades a good deal of research in logic has been prompted by the realization that logical systems can be successfully employed to formalize and solve a variety of computational problems. Traditionally, the theoretical framework for most applications was assumed to be classical logic. However, this assumption often turned out to clash with researchers’ intuitions even in well-established areas of application. Let us consider, for example, what is probably the most representative of these application areas: logic programming The idea that the execution of a Prolog program is to be understood as a derivation in classical logic has played a key role in the development of the area. This interpretation is the leitmotiv of Kowalski’s well-known [1979], whose aim is described as an attempt ‘to apply the traditional methods of [classical] logic to contemporary theories of problem solving and computer programming’. However, here are some quotations which are clearly in conflict with the received view (and with each other) as to the correct interpretation of logic programs:

Relevance Logic not only shows promise as a standard for modular reasoning systems, but it has, in a sense, been already adopted by artificial intelligence researchers. The resolution method for Horn clauses appears to be based on classical logic, but procedural derivation (see [Kowalski, 1979]), the method actually used for logic programming, is not complete for classical logic, and is in fact equivalent to Relevance Logic.[...] the systems of modules which are actually used in computer science have the feature that relevance, not classical logic, provides a theory of their behaviour. [Carson, 1989, p.214]

According to the standard view, a logic program is a definite set of Horn clauses. Thus logic programs are regarded as syntactically restricted first-order theories within the framework of classical logic. Correspondingly, the proof-theory of logic programs is considered as a specialized version of classical resolution, known as SLD-resolution. This view, however, neglects the fact that a program clause a ₀ ← a _l, a ₂, ..., a _n , is an expression of a fragment of positive logic [a subsystem of Intuitionistic Logic] rather than an implication formula of classical logic. The logical behaviour of such clauses is in no way related to any negation or complement operation. So (positive) logic programs are ‘sub-classical’. The classical interpretation seems to be a semantical overkill’ [Wagner, 1991, p.835].