Partial models and logic programming

AbstractThree extensions of the standard Prolog fixpoint semantics are presented (called sat, strong, and weak), using partial models, models which may fail to assign truth values to all formulas. Each of these semantics takes negation and quantification into account. All thee are conservative: they agree with the conventional semantics on pure Horn clause programs. The sat and the strong semantics incorporate the domain closure assumption, but differ on whether to assign a truth value to a classically valid formula some part of which lacks a truth value. The weak semantics is similar to the strong semantics but abandons the domain closure condition, and consequently, all programs give rise to continuous operators in this semantics. For the weak semantics, a sound and complete proof procedure is given, based on semantics tableaus (or equivalently, Gentzen Sequents)