ECAI 2004 Conference Paper

[PDF] [full paper] [prev] [tofc] [next]

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.

[prev] [tofc] [next]

ECAI-2004 is organised by the European Coordinating Committee for Artificial Intelligence (ECCAI) and hosted by the Universitat Politècnica de València on behalf of Asociación Española de Inteligencia Artificial (AEPIA) and Associació Catalana d'Intel-ligència Artificial (ACIA).