Foundations of Paraconsistent Resolution

Article type: Research Article

Authors: Kamide, Norihiro

Affiliations: Department of Philosophy, Keio University, 2-15-45 Mita, Minatoku, Tokyo, 108-8345, Japan. E-mail: kamide@mtc.biglobe.ne.jp

Abstract: An extended first-order predicate sequent calculus PLK with two kinds of negation is introduced as a basis of a new resolution calculus PRC (paraconsistent resolution calculus) for handling the property of paraconsistency. Herbrand theorem, completeness theorem (with respect to a classical-like semantics) and cut-elimination theorem are proved for PLK. The correspondence between PLK and PRC is shown by using a faithful embedding of PLK into the sequent calculus LK for classical logic.

Keywords: Paraconsistent resolution, sequent calculus, Herbrand theorem, completeness, cut-elimination

Journal: Fundamenta Informaticae, vol. 71, no. 4, pp. 419-441, 2006