ECAI 2004 Conference Paper

[full paper]

A Unit Resolution-Based Approach to Tractable and Paraconsistent Reasoning

Sylvie Coste-Marquis, Pierre Marquis

A family of unit resolution-based 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, Resource-Bounded Reasoning, Automated Reasoning, Satisfiability Testing

Citation: Sylvie Coste-Marquis, Pierre Marquis: A Unit Resolution-Based 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.803-807.