
[full paper] 
Sylvie CosteMarquis, Pierre Marquis
A family of unit resolutionbased paraconsistent inference relations $\vdash_{\Sigma}^*$ for propositional logic in the clausal case is introduced. Parameter $\Sigma$ is any consistent set of clauses representing the beliefs which are intended to be exploited through full deduction, i.e., every classical consequence of $\Sigma$ must be kept w.r.t. $\vdash_{\Sigma}^*$, whatever the belief base $B$. Contrariwise to many paraconsistent inference relations, any relation $\vdash_{\Sigma}^*$ can be decided in time linear in $B$ whenever $\Sigma$ is of bounded size. We show that $\vdash_{\Sigma}^*$ exhibits several valuable properties, including strong paraconsistency. We also show how a unit propagation algorithm can be simply turned into a decision procedure for $\vdash_{\Sigma}^*$. We finally show how the $\vdash_{\Sigma}^*$ family relates to several inference relations proposed so far as approximations of classical entailment.
Keywords: Belief Revision, ResourceBounded Reasoning, Automated Reasoning, Satisfiability Testing
Citation: Sylvie CosteMarquis, Pierre Marquis: A Unit ResolutionBased Approach to Tractable and Paraconsistent Reasoning. In R.López de Mántaras and L.Saitta (eds.): ECAI2004, Proceedings of the 16th European Conference on Artificial Intelligence, IOS Press, Amsterdam, 2004, pp.803807.