Specification and initialization of a logic computer system

A logic computer system consists of an inference machine and a compatible logic operating system. This paper describes prospective models for a logic computer system, and its hardware and software components. The language Concurrent Prolog serves as the single implementation, specification, and machine language. The computer system is represented as a logic programming goallogic_computer_system. Specification of the system corresponds to resolution of this goal. Clauses used to solve the goal — and ensuing subgoals — progressively refine the machine, operating system, and computer system designs. In addition, the accumulation of all clauses describing the logic operating system constitute its implementation. Logic computer systems with vastly different fundamental characteristics can be concisely specified in this manner. Two contrasting examples are given and discussed. An important characteristic of both peripheral devices and the overall computer system, whether they are restartable or perpetual, is examined. As well, a method for operational initialization of the logic computer system is presented. The same clauses which incrementally specify characteristics of the computer system also describe the manner in which this initialization takes place.     

Attributed Variables in XSB

The attributed variable data type plays an important role in many extensions to the basic Logic Programming language. It provides a flexible mechanism to implement constraint solvers over different domains in a standard logic programming system. To combine the technique of constraint solving with tabling and build a tabled constraint logic programming system, special work has to be done to handle attributed variables when they are copied into and out of tables. In this paper, we describe the implementation of attributed variables in XSB — a tabled logic programming system.We first introduce the internal representation of attributed variables and the interface between the internal representation and the user defined high level unification handler. Then, as the primary focus of the paper, we describe how the tabling mechanism in XSB can be extended to efficiently handle attributed variables. To save attributed variables in tables, the structure of subgoal table and answer table is modified, and the tabling engine itself requires extension as well.     

Simplifying dynamic programming via mode‐directed tabling

In the dynamic programming paradigm the value of an optimal solution is recursively defined in terms of optimal solutions to subproblems. Such dynamic programming definitions can be tricky and error‐prone to specify. This paper presents an elegant method based on tabled logic programming (TLP) that simplifies the specification of such dynamic programming solutions. Our method introduces a new mode declaration for tabled predicates. The arguments of each tabled predicate are divided into indexed and non‐indexed arguments so that tabled predicates can be regarded as functions: indexed arguments represent input values and non‐indexed arguments represent output values. The non‐indexed arguments in a tabled predicate can be further declared to be aggregated, for example, the minimum, so that while generating answers, the global table will dynamically maintain the smallest value for that argument. This mode‐declaration scheme, coupled with recursion, provides an easy‐to‐use method for dynamic programming: there is no need to define the value of an optimal solution recursively, as the definition of a general solution suffices. The optimal value as well as its corresponding concrete solution can be derived implicitly and automatically using tabled logic programming systems. Our experimental results show that mode declarations improve performance in solving dynamic programming problems on TLP systems. Copyright © 2007 John Wiley & Sons, Ltd.     

A meta-planning model for diminishing resource problems

We present a planning and meta-planning model for an important sub-class of the general planning problem. There is a fixed amount of initial resource which monotonically diminishes throughout the planning process. Assuming all subgoals must be achieved, we have created a commonsense meta-planning methodology based on two policies, graceful retreat and least impact, which have the spirit of cooperation among subgoals in making commitments. Graceful retreat allows the most critical subgoal to be achieved first, at the expense of taking some resource potentially useful to some less critical subgoals. Least impact selects the subplan, to achieve that critical subgoal, which uses resource judged least critical to as yet unachieved subgoals.     

Implementation of tabled evaluation with delaying in Prolog

Unlike SLD resolution as implemented in Prolog, tabled evaluation with delaying guarantees termination for function free logic programs, avoids repeated computation of identical subqueries, and handles recursion through negation. It is often used in query processing and nonmonotonic reasoning where termination is required. The paper presents a new technique for incorporating tabled evaluation into existing Prolog systems. It requires neither time consuming modifications of a Prolog engine nor metainterpretation that can enormously slow down program execution. Instead, using a program transformation approach, the technique allows effective use of the advanced Prolog technology. The transformed program uses tabling primitives implemented externally in C that provide direct control over the search strategies. This brings efficiency as well as portability across Prolog systems. Experiences with a prototype implementation indicate that the approach results in a flexible and pragmatic method for query processing and nonmonotonic reasoning on top of Prolog. Performance measurements show that the method is efficient for practical applications     

Complete logic programs with domain-closure axiom

Complete logic programs augmented with the domain-closure axiom are proposed as the reference theory for logic programming with negation as failure. An inference rule corresponding to “proof by case analysis” is proved correct within this framework. As a major consequence, the completeness results for SLD resolution and negation as failure still hold. An interesting outcome is that some novel operational properties of SLD resolution can be proved.     

Logic programming with arrays

Nial is a programming language designed around a mathematical treatment of data as nested arrays. A goal of the research described is to integrate within Nial a functional style of programming based on the theory of arrays with the declarative capabilities of a logic programming environment. This is partially accomplished by storing logic clauses as arrays which can be manipulated using logic clauses. Arrays as terms are considered as part of the syntax of the clauses. The approach to logic programming is based on providing a flexible environment for experimenting with full clausal or Horn clause logic. A variety of predefined control strategies and the capability for user-defined control strategies have been provided. The expressive capabilities of combining logic and functional programming styles provides a suitable language for many application areas. The philosophy and design behind a combined logic/database model used to prototype a knowledge-based systems application are described     

Efficient access mechanisms for tabled logic programs

The use of tabling in logic programming allows bottom-up evaluation to be incorporated in a top-down framework, combining advantages of both. At the engine level, tabling also introduces issues not present in pure top-down evaluation, due to the need for subgoals and answers to access tables during resolution. This article describes the design, implementation, and experimental evaluation of data structures and algorithms for high-performance table access. Our approach uses tries as the basis for tables. Tries, a variant of discrimination nets, provide complete discrimination for terms, and permit a lookup and possible insertion to be performed in a single pass through a term. In addition, a novel technique of substitution factoring is proposed. When substitution factoring is used, the access cost for answers is proportional to the size of the answer substitution, rather than to the size of the answer itself. Answer tries can be implemented both as interpreted structures and as compiled WAM-like code. When they are compiled, the speed of computing substitutions through answer tries is competitive with the speed of unit facts compiled or asserted as WAM code. Because answer tries can also be created an order of magnitude more quickly than asserted code, they form a promising alternative for representing certain types of dynamic code, even in Prolog systems without tabling.     

A simplified problem reduction format

Some new approaches to mechanical theorem proving in the first-order predicate calculus are presented. These are based on a natural deduction system which can be used to show that a set of clauses is inconsistent. This natural deduction system distinguishes positive from negative literals and treats clauses having 0, 1, and 2 or more positive literals in three separate ways. Several such systems are presented. The systems are complete and relatively simple and allow a goal to be decomposed into subgoals, and solutions to the subgoals can then be searched for in the same way. Also, the systems permit a natural use of semantic information to delete unachievable subgoals. The goal-subgoal structure of these systems should allow much of the current artificial intelligence methodology to be applied to mechanical theorem proving.     

利用算符分析的问题求解

将状态空间的问题求解过程变换为逐步缩小与目标状态的差异过程是一种问题的分解方式．求解差异的顺序可通过分析算符对状态的影响而作出规划，规划的原则是最大限度地在不改变最近已实现子目标的条件下实现下一子目标．为此，在问题分解时各层子目标选择的依据是让各算符有最大的可利用率，即以状态对算符最小约束传播的原则选择各层子目标；最后生成一个子目标规划层次集．问题求解过程就表现为从初始状态开始实现层次集中的某一子目标序列，其间可能涉及子目标回溯．     

Concurrent Query Processing for Logic Inference Using the Connection Graph

Some logic program may have to process a sequence of asynchronously arriving concurrent queries. We provide a tagging scheme for resolution in the Connection Graph that allows later queries to reuse the work done for earlier or concurrent queries. The scheme can be used either by a sequential or a parallel logic inference system that uses the Connection Graph proof procedure. Our scheme is justified in terms of multiplexing multiple virtual Connection Graphs on one physical data structure. The tagging scheme is presented as a set of rules which are proved to be correct. An important characteristic of the Connection Graph procedure is the ability to delete clauses containing pure literals. In the proposed scheme, it is necessary to weaken it. Given some information about the form of incoming queries, we can strengthen this capability. If earlier links are allowed to be reconstructed, then the ability can be regained fully, via a caching scheme.     

Dynamic generation of subgoals for autonomous mobile robots usinglocal feedback information

An algorithm is presented for using a local feedback information to generate subgoals for driving an autonomous mobile robot (AMR) along a collision-free trajectory to a goal. The subgoals section algorithm (SSA) updates subgoal positions while the AMR is moving so that continuous motion is achieved without stopping to replan a path when new sensor data becomes available. Assuming a finite number of polynomial obstacles (i.e. the internal representation of the local environment in terms of a 2-D map with linear obstacles boundaries) and a dynamic steering control algorithm (SCA) capable of driving the AMR to safe subgoals, it is shown that the feedback algorithm for subgoal selection will direct the AMR along a collision-free trajectory to the final goal in finite time. Properties of the algorithm are illustrated by simulation examples     

Induction as Consequence Finding

This paper presents a general procedure for inverse entailment which constructs inductive hypotheses in inductive logic programming. Based on inverse entailment, not only unit clauses but also characteristic clauses are deduced from a background theory together with the negation of positive examples. Such clauses can be computed by a resolution method for consequence finding. Unlike previous work on inverse entailment, our proposed method called CF-induction is sound and complete for finding hypotheses from full clausal theories, and can be used for inducing not only definite clauses but also non-Horn clauses and integrity constraints. We also show that CF-induction can be used to compute abductive explanations, and then compare induction and abduction from the viewpoint of inverse entailment and consequence finding.     

Filter-based resolution principle for lattice-valued propositional logic LP(X)

As one of most powerful approaches in automated reasoning, resolution principle has been introduced to non-classical logics, such as many-valued logic. However, most of the existing works are limited to the chain-type truth-value fields. Lattice-valued logic is a kind of important non-classical logic, which can be applied to describe and handle incomparability by the incomparable elements in its truth-value field. In this paper, a filter-based resolution principle for the lattice-valued propositional logic LP(X) based on lattice implication algebra is presented, where filter of the truth-value field being a lattice implication algebra is taken as the criterion for measuring the satisfiability of a lattice-valued logical formula. The notions and properties of lattice implication algebra, filter of lattice implication algebra, and the lattice-valued propositional logic LP(X) are given firstly. The definitions and structures of two kinds of lattice-valued logical formulae, i.e., the simple generalized clauses and complex generalized clauses, are presented then. Finally, the filter-based resolution principle is given and after that the soundness theorem and weak completeness theorems for the presented approach are proved.     

Dynamic steering control of conventionally steered mobile robots

This article presents an algorithm for dynamically steering an autonomous mobile robot (AMR) along a collision-free path to a goal using local feedback information. A twolevel navigation algorithm is presented in which a subgoal selection algorithm (SSA) generates visible subgoals to be pursued by the steering control algorithm (SCA). An earlier article presented the SSA in detail, demonstrating how subgoals can be updated while the AMR is moving so that a continuous motion is achieved without stopping to replan the path when new sensor data become available. This study focuses on the SCA. In particular, a general feedback scheme is developed for dynamically steering an AMR to a visible goal in the local obstacle-free space identified by the SSA. We present the detailed implementation of the SCA for a conventionally steered AMR (CAMR). Simulation results are presented that demonstrate the effectiveness of the combined SSA-SCA feedback scheme. The algorithm has been successfully implemented on the NavLab at CMU.     

Pattern Databases

The efficiency of A* searching depends on the quality of the lower bound estimates of the solution cost. Pattern databases enumerate all possible subgoals required by any solution, subject to constraints on the subgoal size. Each subgoal in the database provides a tight lower bound on the cost of achieving it. For a given state in the search space, all possible subgoals are looked up in the pattern database, with the maximum cost over all lookups being the lower bound. For sliding tile puzzles, the database enumerates all possible patterns containing N tiles and, for each one, contains a lower bound on the distance to correctly move all N tiles into their correct final location. For the 15-Puzzle, iterative-deepening A* with pattern databases(N ="8) reduces the total number of nodes searched on a standard problem set of 100 positions by over 1000‐fold.     

Profiling prolog programs

Profilers play an important role in the development of efficient programs. Profiling techniques developed for traditional languages are inadequate for logic programming languages, for a number of reasons: first, the flow of control in logic programming languages, involving back-tracking and failure, is significantly more complex than in traditional languages; secondly, the time taken by a unification operation, the principal primitive operation of such languages, cannot be predicted statically because it depends on the size of the input; and finally, programs may change at run-time because clauses may be added or deleted using primitives such as assert and retract. This paper describes a simple profiler for Prolog. The ideas outlined here may be used either to implement a simple interactive profiler, or integrated into Prolog compilers.     

Discovering rules to design newspapers: An inductive constraint logic programming approach

Inductive logic programming combines both machine learning and logic programming techniques. ILP uses first-order predicate logic restricted to Horn clauses as an underlying language. Thus, programs induced by an ILP system inherit the classical limitations of PROLOG programs. Constraint logic programming avoids some of the limitations of logic programming, and so ILP aims to induce programs that employ this paradigm. Current ILP systems that induce constrained logic programs extend systems based on the normal semantics ofILP. In this article we introduce IC-Log, a new system that induces constrained logic programs and relies on an extension ofa nonmonotonic semantics-based system. We then present an application of IC-Log in the field ofcomputer-aided publishing.     

Implementing tactics and tacticals in a higher-order logic programming language

We argue that a logic programming language with a higher-order intuitionistic logic as its foundation can be used both to naturally specify and implement tactic-style theorem provers. The language extends traditional logic programming languages by replacing first-order terms with simply-typed -terms, replacing first-order unification with higher-order unification, and allowing implication and universal quantification in queries and the bodies of clauses. Inference rules for a variety of inference systems can be naturally specified in this language. The higher-order features of the language contribute to a concise specification of provisos concerning variable occurrences in formulas and the discharge of assumptions present in many inference systems. Tactics and tacticals, which provide a framework for high-level control over search for proofs, can be directly and naturally implemented in the extended language. This framework serves as a starting point for implementing theorem provers and proof systems that can integrate many diversified operations on formulas and proofs for a variety of logics. We present an extensive set of examples that have been implemented in the higher-order logic programming language Prolog.     

Extremal problems in logic programming and stable model computation

We study the following problem: given a class of logic programs ¢, determine the maximum number of stable models of a program from ©. We establish the maximum for the class of all logic programs with at most n clauses, and for the class of all logic programs of size at most n. We also characterize the programs for which the maxima are attained. We obtained similar results for the class of all disjunctive logic programs with at most n clauses, each of length at most m, and for the class of all disjunctive logic programs of size at most n. Our results on logic programs have direct implication for the design of algorithms to compute stable models. Several such algorithms, similar in spirit to the Davis-Putnam procedure, are described in the paper. Our results imply that there is an algorithm that finds all stable models of a program with n clauses after considering the search space of size O(3^n/3) in the worst case. Our results also provide some insights into the question of representability of families of sets as families of stable models of logic programs.