@article {D:ppp_cl,
	title = {A Paraconsistent Proof Procedure Based on Classical Logic},
	year = {2003},
	abstract = {<p>Apparently Ex Falso Quodlibet (or Explosion) cannot be isolated within CL (Classical Logic); if Explosion has to go, then so have other inference rules, for example either Addition or Disjunctive Syllogism. This cer- tainly holds according to the standard abstract view on logic. However, as I shall show, it does not hold if a logic is defined by a procedure-a set of instructions to obtain a proof (if there is one) of a given conclusion from a given premise set. In this paper I present a procedure pCL{\textexclamdown} that defines a logic CL{\textexclamdown}|a function assigning a consequence set to any premise set. Anything deriv- able by CL from a consistent premise set {\textexclamdown} is derivable from {\textexclamdown} by CL{\textexclamdown}. If {\textexclamdown} is (CL-)inconsistent, pCL{\textexclamdown} enables one to demonstrate this (by de- riving a contradiction from {\textexclamdown}). The logic CL{\textexclamdown} validates applications of Disjunctive Syllogism as well as applications of Addition. Nevertheless, this logic is paraconsistent as well as (in a specific sense) relevant. pCL{\textexclamdown} derives from an intuitively attractive proof search procedure. A characteristic semantics for CL{\textexclamdown} will be presented and the central prop- erties of the logic will be mentioned. CL{\textexclamdown} shows that (and clarifies how) adherents of CL may obtain non-trivial consequence sets for inconsistent theories.</p>},
	author = {Batens, Diderik}
}
