=Paper=
{{Paper
|id=Vol-3072/paper11
|storemode=property
|title=Inference From Non-Horn Clauses With Partial Predicates
|pdfUrl=https://ceur-ws.org/Vol-3072/paper11.pdf
|volume=Vol-3072
|authors=Alexander Sakharov
|dblpUrl=https://dblp.org/rec/conf/ictcs/Sakharov21
}}
==Inference From Non-Horn Clauses With Partial Predicates==
https://ceur-ws.org/Vol-3072/paper11.pdf
Inference From Non-Horn Clauses With Partial
Predicates (short paper)?
Alexander Sakharov
Synstretch, Framingham, Massachusetts, USA
Abstract. This paper investigates inference without Reductio Ad Ab-
surdum from knowledge bases comprised of non-Horn rules with partial
predicates and functions. The semantics of this inference is specified by
3-valued models with constraints. This inference corresponds to model
elimination without the reduction rule, which is equivalent to input reso-
lution and to chaining extended with rule contrapositives. It is character-
ized by sequent calculi without the contraction rule and with non-logical
axioms expressing rules and facts.
1 Introduction
The rules of knowledge bases (KB) are usually quantifier-free expressions A ⇐
A1 ∧ ... ∧ Ak , where A, A1 , ..., Ak are literals. KB facts are literals. Sets of these
facts and rules are also called logic programs. These rules are equivalent to (non-
Horn) clauses, i.e disjunctions of literals, in classical first-order logic (FOL).
These rules and facts as well as the respective KBs will be called non-Horn [11].
In normal logic programs, A is an atom. Prolog comprises Horn rules in which A
and all Ai are atoms. The goals of inference from KBs (aka queries) are literals
as opposed to arbitrary formulas for FOL theorem provers.
Many tasks are most conveniently specified by a combination of facts, rules,
and computable functions. Some existing inference systems include computable
(evaluable) functions and predicates [5]. These functions are built-in or user-
defined recursive functions. We assume that evaluable functions may occur in
terms that are predicate arguments, and predicates may be defined as boolean
recursive functions as well. In author’s opinion, any KB inference system should
incorporate computable functions and predicates in order to be practical. Inte-
gration of KBs and recursive functions may go further by allowing predicates
specified by KB rules in the definitions of recursive functions.
Evaluable functions and predicates may be partial. Other predicates should
also be considered partial by default. First, rule sets are often incomplete and
some atoms with constant arguments are not derivable in FOL from KB rules and
facts, and their negations are not derivable either. Second, some non-evaluable
predicates are inherently partial from the proof-theoretical perspective. It is well-
known that any partial recursive function can be represented by Horn rules.
?
Copyright 2021 for this paper by its authors. Use permitted under Creative Com-
mons License Attribution 4.0 International (CC BY 4.0).
Consider function f (x) whose domain is undecidable [8] and whose range is
a known finite set. If predicate P represents f , then it is impossible that the
derivation of either P (a, b) or ¬P (a, b) succeeds for any constants a, b. Detecting
atoms with defined truth values is an undecidable problem [8].
The principle of Reductio Ad Absurdum (RAA) states that A is derivable if it
is derivable from hypothesis ¬A. In author’s opinion, the legitimacy of reasoning
by contradiction, i.e. with using RAA, is questionable in the presence of partial
predicates or functions. It seems faulty to apply RAA when the truth value of
the hypothesis is undefined. Intuitionists criticized the law of excluded middle
in regard to statements about infinite collections. This criticism is even more
relevant to RAA in the presence of partial predicates and functions.
The aim of this paper is to investigate inference from non-Horn KBs without
RAA in presence of evaluable predicates and functions. Unlike Horn KBs, infer-
ence from non-Horn KBs without reasoning by contradiction utilizes negation
properties. Non-Horn KBs avoid controversies arising from relying on negation
as failure [3]. This short paper is a summary of results, proofs are only sketched,
and a review of related work is omitted.
The semantics of inference from non-Horn KBs without reasoning by con-
tradiction can be specified by natural 3-valued models [1] with constraints. The
third value represents undefined truth values of partial predicates and of atoms
with undefined arguments. Inference from non-Horn KBs without RAA corre-
sponds to model elimination without the reduction rule, which is equivalent to
input resolution and to forward/backward chaining extended with rule contra-
positives. This inference is characterized by sequent calculi without the contrac-
tion rule and with non-logical axioms expressing rules and facts.
2 Extended Chaining, Resolution, Model Elimination
A literal is called ground if it does not contain variables. A substitution is a finite
set of mappings of variables to terms. The result of applying a substitution to a
formula or set of formulas is called its instance. We assume that occurrences of
evaluable functions/predicates with constant arguments are evaluated as soon as
they appear in derivations. Any complete search strategy for inference from KBs
with evaluable functions/predicates should conduct and-or search [9] simultane-
ously with evaluations. A KB is called consistent if no atom is derivable from
this KB along with its negation.
If A is an evaluable predicate and the evaluation of ground literal A(...) yields
true, then A(...) is considered a fact. If the evaluation of literal A(...) yields false,
then ¬A(...) is considered a fact. These facts are not physically stored in KBs.
There could be an infinite number of them.
Forward and backward chaining are widely used as inference methods for
Horn KBs with goals (queries) that are atoms. These two methods can be applied
to non-Horn KBs or non-Horn logic programs and to goals that are literals. Both
forward and backward chaining are based on Generalized Modus Ponens as the
sole inference rule [9]: if A01 ...A0k are derived literals, A ⇐ A1 ∧ ... ∧ Ak is a rule,
substitution θ is a unifier of literals A0i and Ai , i.e. A0i θ = Ai θ for i = 1...k,
then Aθ is derivable. For facts, k = 0. A forward chaining step derives Aθ
given that A01 , ..., A0k are derived literals. Given goal list L = {...G...} and such
substitution θ that Gθ = Aθ, every step of backward chaining replaces goal
G with A1 θ, ..., Ak θ in L and also applies θ to the other goals in L. Forward
and backward chaining have the same inference power. Negation is redundant
in backward and forward chaining.
For any rule A ⇐ A1 ∧ ... ∧ Ak , the following implications ∼ Ai ⇐∼ A ∧ A1 ∧
...Ai−1 ∧ Ai+1 ... ∧ An are called contrapositives to this rule [11]. ∼ A denotes
the complement of literal A. Rules entail their contrapositives in classical FOL.
Chaining methods can be extended by adding contrapositives to rules. This may
significantly increase the range of derivable literals. For instance, if literals P (a)
and R(a) are facts, then literal ¬Q(a) is derivable by forward and backward
chaining with contrapositives from rules A(x) ⇐ P (x), ¬A(x) ⇐ Q(x) ∧ R(x).
This derivation is not possible without contrapositives. Contrapositives make
use of negation properties. We will refer to forward and backward chaining with
contrapositives as extended chaining.
The resolution calculus [2] has two rules: resolution and factoring. The reso-
lution rule produces clause A1 θ ∨ ... ∨ Ak θ ∨ B1 θ ∨ ... ∨ Bm θ from two clauses
A1 ∨ ... ∨ A ∨ ... ∨ Ak and B1 ∨ ... ∨ B ∨ ... ∨ Bm where substitution θ is the
most general unifier (MGU) of A and ∼ B, that is, any other unifier of the two
literals is a composition of θ and another substitution. The factoring rule pro-
duces clause A1 θ ∨ ... ∨ Aθ ∨ ... ∨ Ak θ from clause A1 ∨ ... ∨ A ∨ ... ∨ A0 ∨ ... ∨ Ak
where θ is the MGU of A and A0 . In input resolution, one of two premises of the
resolution rule is a clause from the input set [2].
The PTTP model elimination procedure [11] has two rules and uses con-
trapositives. Its resolution rule produces goal list A1 θ, ..., Ak θ, [Bθ], B1 θ, ..., Bm θ
from rule or contrapositive A ⇐ A1 , ..., Ak and goal list B, B1 , ..., Bm where θ is
the MGU of A and B. Leftmost framed literals are removed immediately. The
reduction rule produces B1 θ, ..., [B 0 θ], ..., Bm θ from B, B1 , ..., [B 0 ], ..., Bm where
θ is the MGU of ∼ B and B 0 . This procedure gives a characterization of proofs
by contradiction. They are the model elimination derivations involving the re-
duction rule since this rule is essentially RAA. It eliminates a hypothesis in the
case that this hypothesis implies its complement.
Theorem 1. Literal L is derivable by extended chaining if and only if ∼ L is
refutable by input resolution in which KB rules/facts are input clauses and ∼ L
is used in the first resolution step only.
Theorem 2. Literal L is derivable by the PTTP model elimination procedure
without the reduction rule if and only if ∼ L is refutable by input resolution in
which ∼ L is used in the first resolution step only.
Factoring is admissible in resolution refutations satisfying the condition of
Theorem 1. Input resolution steps map to backward chaining steps. The lifting
lemma [2] guarantees that chaining derivations can be mapped to input resolu-
tion refutations. Any PTTP derivation not using the reduction rule is a resolution
refutation satisfying the condition of Theorem 2. Input resolution refutations are
transformed to PTTP derivations by iteratively adjusting the order of resolution
steps.
Taken together, Theorem 1 and Theorem 2 show that extended chaining
derivations and input resolution refutations coincide with FOL derivations with-
out using RAA. All of them correspond to direct derivations used in formal
argumentation. Direct derivations are defined as natural deduction done with-
out using RAA [4]. Every literal occurring in any successful extended chaining
derivation is derivable as well [10]. This property can be reformulated for input
resolution and model elimination, it is characteristic of KB inference without
RAA. Inference without RAA is not the same as intuitionistic inference. It does
not correspond to an intermediate logic either [6].
3 3-Valued Models
Semantically in the context of non-Horn KBs, a ground atom may be neither
true nor false. Hence, classical 2-valued FOL models are not adequate in the
presence of partial functions and predicates. Models for non-Horn KBs should
have at least three values: −1 (false), 1 (true), 0 (undefined). These values are
assigned to all ground atoms. The meaning of 0 is that constant arguments of
the predicate are outside of its domain or an evaluable function occurring in the
atom does not yield a value. Fortunately, three values are sufficient for models
that are relevant to KB inference without RAA.
Multi-valued models are usually defined by truth tables (or functions) for
logical connectives so that the truth values of ground formulas can be calculated.
Let |A| denote the truth value of ground literal A. The following equation defines
the truth values for negation: |¬A| = −|A|. This definition complies with natural
3-valued logics [1].
KB inference is only concerned with literals as the outcome of any deriva-
tion step. No other formulas are produced during derivations. Because of this,
legitimate models for KB inference can be defined by the above negation truth
function and by constraints on truth values in ground instances of facts and rules
as opposed to truth tables for other connectives. These constraints are:
1. A is a ground fact instance: |A| = 1
2. A0 ⇐ A1 ∧ ... ∧ Ak is a ground rule instance:
a. If |Ai | = 1 for i = 1...k, then |A0 | = 1.
b. If |A0 | = −1 and |Ai | = 1 for i = 1...j − 1, j + 1...k, then |Aj | = −1.
Models satisfying these constraints will be denoted M. Ground literal A is valid
if |A| = 1 for all M models.
Theorem 3. Extended chaining is sound and complete with respect to M models
for consistent KBs.
The proof of soundness for Theorem 3 is straightforward. To prove the com-
pleteness, we consider a model in which every derivable literal is true, its com-
plement is false, and the truth value of every other literal is undefined. Assume
|A| = 1 in all M models for ground literal A and it is not derivable by extend-
ed chaining from KB facts and rules. It can be proved that the model under
consideration satisfies the M constraints, and thus, our assumption is incorrect.
4 Sequent Calculi
We rely on sequent calculi with non-logical axioms as an instrument for logical
characterization of KB inference without RAA. A sequent is Γ ` Π where Γ is
an antecedent and Π is a succedent. Consider a variant of Gentzen’s LK [12] in
which antecedents and succedents are multisets of formulas instead of sequences.
This variant eliminates the need in the exchange rule. LK has one logical axiom
A ` A. Let us exclude the contraction rule. The remaining structural rules are
cut and weakening:
Γ ` A, ∆ A, Π ` Σ Γ `Π Γ `Π
cut LW RW
Γ, Π ` ∆, Σ A, Γ ` Π Γ ` A, Π
Instances of this sequent calculus incorporating non-logical axioms will be de-
noted LK−c .
KB inference and logic programming are concerned about the derivation of
sequents of the form ` A in the terminology of sequent calculi, A is a literal. KB
facts and rules can be treated as non-logical axioms [6]. Sequents of the form ` A
represent facts, and rules are represented by sequents of the form A1 , ..., An ` A
where A, A1 , ..., Ak are literals. Variables can be replaced by terms in instances
of these axioms.
Whereas cut is essential in LK−c , cut elimination techniques can be applied
to the logical rules for connectives ∧, ∨, ⇒ and for quantifiers. They are admis-
sible in derivations of literals and so are all formulas except for literals [6]. The
only logical rules that are necessary in these derivations are two negation rules:
Γ ` A, Π A, Γ ` Π
L¬ R¬
¬A, Γ ` Π Γ ` ¬A, Π
Theorem 4. Any LK−c derivation of literal G can be transformed into an ex-
tended chaining derivation and vice versa provided that the KB is consistent.
The proof that a backward chaining derivation with contrapositives can be
transformed into a LK−c derivation is straightforward. Consider a LK−c deriva-
tion that does not contain other formulas than literals. Weakening is admissible
in such derivations. This derivation can be transformed into another derivation
in which one of two premises of every cut is a descendant of axiom G ` G, and
the other is a fact or rule possibly modified by negation rules. The transformed
derivation maps to a chaining derivation.
Theorem 4 guarantees that extended chaining is complete for derivation of
literals in LK−c given that a complete search strategy is employed. Here is a
description of the difference between inference without RAA and intuitionistic
logic: LK without contraction is equivalent to LJ without contraction and with
the axiom of double negation [7]. The M constraints can be reformulated for
non-logical axioms of LK−c instead of KB rules and facts.
Corollary 1. Derivation of literals in LK−c is sound and complete with respect
to M models for consistent KBs.
References
1. Avron, A.: Natural 3-valued logics–characterization and proof theory. The Journal
of Symbolic Logic 56(1), 276–294 (1991)
2. Chang, C.L., Lee, R.C.T.: Symbolic logic and mechanical theorem proving. Aca-
demic press (1973)
3. Denecker, M., Truszczynski, M., Vennekens, J.: About negation-as-failure and
the informal semantics of logic programming. Association for Logic Programming
(2017)
4. Kakas, A.C., Mancarella, P., Toni, F.: On argumentation logic and propositional
logic. Studia Logica 106(2), 237–279 (2018)
5. McCune, W.: Otter 3.3 reference manual and guide. Tech. rep., Argonne National
Lab. (2003)
6. Negri, S., Von Plato, J.: Structural proof theory. Cambridge University Press (2001)
7. Ono, H.: Logics without the contraction rule and residuated lattices. Australasian
Journal of Logic (2010)
8. Rogers, H.: Theory of recursive functions and effective computability. McGraw-Hill
Book Co. (1967)
9. Russell, S., Norvig, P.: Artificial Intelligence: A Modern Approach. Prentice Hall
Press, 3rd edn. (2009)
10. Sakharov, A.: A best-first backward-chaining search strategy based on learned
predicate representations. In: 13th International Conference on Agents and Artifi-
cial Intelligence. pp. 982–989 (2021)
11. Stickel, M.E.: A Prolog technology theorem prover: a new exposition and imple-
mentation in Prolog. Theoretical Computer Science 104(1), 109–128 (1992)
12. Szabo, M.E. (ed.): The collected papers of Gerhard Gentzen. North-Holland (1969)