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)