Inference From Non-Horn Clauses With Partial Predicates (short paper)?

Abstract

This paper investigates inference without Reductio Ad Absurdum from knowledge bases comprised of non-Horn rules with partial predicates and functions. The semantics of this inference is speci ed by 3-valued models with constraints. This inference corresponds to model elimination without the reduction rule, which is equivalent to input resolution and to chaining extended with rule contrapositives. It is characterized by sequent calculi without the contraction rule and with non-logical axioms expressing rules and facts.

Introduction

Consider function f (x) whose domain is undecidable [ 8 ] and whose range is a known nite 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 de ned 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 unde ned. Intuitionists criticized the law of excluded middle in regard to statements about in nite 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, inference 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 contradiction can be speci ed by natural 3-valued models [ 1 ] with constraints. The third value represents unde ned truth values of partial predicates and of atoms with unde ned arguments. Inference from non-Horn KBs without RAA corresponds to model elimination without the reduction rule, which is equivalent to input resolution and to forward/backward chaining extended with rule contrapositives. This inference is characterized by sequent calculi without the contraction 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 nite 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 ] simultaneously 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 in nite 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 uni er 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 = f:::G:::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 signi cantly 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 resolution rule produces clause A1 _ ::: _ Ak _ B1 _ ::: _ Bm from two clauses A1 _ ::: _ A _ ::: _ Ak and B1 _ ::: _ B _ ::: _ Bm where substitution is the most general uni er (MGU) of A and B, that is, any other uni er of the two literals is a composition of and another substitution. The factoring rule produces 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 contrapositives. 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 ; :::; [B0 ]; :::; Bm from B; B1; :::; [B0]; :::; Bm where is the MGU of B and B0. This procedure gives a characterization of proofs by contradiction. They are the model elimination derivations involving the reduction 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 refutable by input resolution in which KB rules/facts are input clauses and is used in the rst resolution step only.

L is

L 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 rst 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 resolution 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 without using RAA. All of them correspond to direct derivations used in formal argumentation. Direct derivations are de ned as natural deduction done without 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 (unde ned). 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 su cient for models that are relevant to KB inference without RAA.

Multi-valued models are usually de ned by truth tables (or functions) for logical connectives so that the truth values of ground formulas can be calculated. Let jAj denote the truth value of ground literal A. The following equation de nes the truth values for negation: j:Aj = jAj. This de nition complies with natural 3-valued logics [ 1 ].

KB inference is only concerned with literals as the outcome of any derivation step. No other formulas are produced during derivations. Because of this, legitimate models for KB inference can be de ned 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: jAj = 1 2. A0 ( A1 ^ ::: ^ Ak is a ground rule instance: a. If jAij = 1 for i = 1:::k, then jA0j = 1.

b. If jA0j = 1 and jAij = 1 for i = 1:::j 1; j + 1:::k, then jAj j = 1. Models satisfying these constraints will be denoted M. Ground literal A is valid if jAj = 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 completeness, we consider a model in which every derivable literal is true, its complement is false, and the truth value of every other literal is unde ned. Assume jAj = 1 in all M models for ground literal A and it is not derivable by extended chaining from KB facts and rules. It can be proved that the model under consideration satis es 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 A; `` LW ``A; RW Instances of this sequent calculus incorporating non-logical axioms will be denoted 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 quanti ers. They are admissible 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:

A;

` ` :A;

R: Theorem 4. Any LK c derivation of literal G can be transformed into an extended 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 derivation 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 modi ed 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 di erence 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 . Academic 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 e ective computability . McGraw-Hill Book Co . ( 1967 )

9. Russell , S. , Norvig , P. : Arti cial Intelligence: A Modern Approach . Prentice Hall Press, 3rd edn. ( 2009 )

10. Sakharov , A. : A best- rst backward-chaining search strategy based on learned predicate representations . In: 13th International Conference on Agents and Arti - cial Intelligence . pp. 982 { 989 ( 2021 )

11. Stickel , M.E. : A Prolog technology theorem prover: a new exposition and implementation in Prolog . Theoretical Computer Science 104 ( 1 ), 109 { 128 ( 1992 )

12. Szabo , M.E. (ed.): The collected papers of Gerhard Gentzen . North-Holland ( 1969 )