An Almost Classical Logic for Logic Programming and Nonmonotonic Reasoning

TL;DR

This paper introduces N^4, a nearly classical logic that preserves many classical logic features while accommodating fourfold negations, providing a robust semantics for logic programming and nonmonotonic reasoning.

Contribution

It presents N^4, a first-order logic that maintains classical implications and negation distribution, and demonstrates its effectiveness in formalizing semantics of logic programs.

Findings

N^4 reduces fourfold negations instead of eliminating double negations.

Herbrand interpretations in classical logic extend naturally to N^4.

Stable models of logic programs coincide with minimal N^4 Herbrand models.

Abstract

The model theory of a first-order logic called N^4 is introduced. N^4 does not eliminate double negations, as classical logic does, but instead reduces fourfold negations. N^4 is very close to classical logic: N^4 has two truth values; implications in N^4 are material, like in classical logic; and negation distributes over compound formulas in N^4 as it does in classical logic. Results suggest that the semantics of normal logic programs is conveniently formalized in N^4: Classical logic Herbrand interpretations generalize straightforwardly to N^4; the classical minimal Herbrand model of a positive logic program coincides with its unique minimal N^4 Herbrand model; the stable models of a normal logic program and its so-called complete minimal N^4 Herbrand models coincide.