Eliminating Redundant Search Space on Backtracking for Forward Chaining Theorem Proving

This paper introduces some improvements on the intelligent backtrackingstrategy for forward chaining theorem proving. How to decide a minimal useful consequent atom setfor a refutation derived at a node in a proof tree is discussed. In most cases, an unnecessarynon-Horn clause used for forward chaining will be split only once. The increase of the search spaceby invoking unnecessary forward chaining clauses will be nearly linear, not exponential anymore. Inthis paper, the principle of the proposed method and its correctness are introduced. Moreover, someexamples are provided to show that the proposed approach is powerful for forward chaining theoremproving.

Logic Programs,Compatibility and Forward Chaining Construction

Logic programming under the stable model semantics is proposed as a non-monotonic language for knowledge representation and reasoning in artificial intelligence. In this paper, we explore and extend the notion of compatibility and the A operator, which were first proposed by Zhang to characterize default theories. First, we present a new characterization of stable models of a logic program and show that an extended notion of compatibility can characterize stable submodels. We further propose the notion of weak auto-compatibility which characterizes the Normal Forward Chaining Construction proposed by Marek, Nerode and Remmel. Previously, this construction was only known to construct the stable models of FC-normal logic programs, which turn out to be a proper subclass of weakly auto-compatible logic programs. We investigate the properties and complexity issues for weakly auto-compatible logic programs and compare them with some subclasses of logic programs.

A Micro Perspective of Research Dynamics Through“Citations of Citations”Topic Analysis

Purpose:Research dynamics have long been a research interest.It is a macro perspective tool for discovering temporal research trends of a certain discipline or subject.A micro perspective of research dynamics,however,concerning a single researcher or a highly cited paper in terms of their citations and“citations of citations”(forward chaining)remains unexplored.Design/methodology/approach:In this paper,we use a cross-collection topic model to reveal the research dynamics of topic disappearance topic inheritance,and topic innovation in each generation of forward chaining.Findings:For highly cited work,scientific influence exists in indirect citations.Topic modeling can reveal how long this influence exists in forward chaining,as well as its influence.Research limitations:This paper measures scientific influence and indirect scientific influence only if the relevant words or phrases are borrowed or used in direct or indirect citations.Paraphrasing or semantically similar concept may be neglected in this research.Practical implications:This paper demonstrates that a scientific influence exists in indirect citations through its analysis of forward chaining.This can serve as an inspiration on how to adequately evaluate research influence.Originality:The main contributions of this paper are the following three aspects.First,besides research dynamics of topic inheritance and topic innovation,we model topic disappearance by using a cross-collection topic model.Second,we explore the length and character of the research impact through“citations of citations”content analysis.Finally,we analyze the research dynamics of artificial intelligence researcher Geoffrey Hinton’s publications and the topic dynamics of forward chaining.

FC-normal and extended stratified logic program

This paper investigates the consistency property of FC-normal logic program and presents an equivalent deciding condition whether a logic program P is an FC-normal program. The deciding condition describes the characterizations of FC-normal program. By the Petri-net presentation of a logic program, the characterizations of stratification of FC-normal program are investigated. The stratification of FC-normal program motivates us to introduce a new kind of stratification, extended stratification, over logic program. It is shown that an extended (locally) stratified logic program is an FC-normal program. Thus, an extended (locally) stratified logic program has at least one stable model. Finally, we have presented algorithms about computation of consistency property and a few equivalent deciding methods of the finite FC-normal program.