Predicate Synthesis for Correcting Faulty Conjectures: The Proof Planning Paradigm

The synthesis of programs as well as other synthetic tasks often end up with an unprovable, partially false conjecture. A successful subsequent synthesis attempt depends on determining why the conjecture is faulty and how it can be corrected. Hence, it is highly desirable to have an automated means for detecting and correcting faulty conjectures.We introduce a method for patching faulty conjectures. The method is based on abduction and performs its task during an attempt to prove a given conjecture. On input X. G(X), the method builds a definition for a corrective predicate, P(X), such that X. P(X) G(X) is a theorem. The synthesis of a corrective predicate is guided by the constructive principle of formulae as types, relating inference with computation.We take the construction of a corrective predicate as a program transformation task. The method consists of a collection of construction commands. A construction command is a small program that makes use of one or more program editing commands, geared towards building recursive, equational procedures.A synthesised corrective predicate is guaranteed to be correct, turning a faulty conjecture into a theorem. Whether conditional or not, it will be well-defined. If recursive, it will also be terminating.Our method is amenable to mechanisation, but careful search guidance is required for making a productive use of the failure of a proof. A failed proof attempt quickly yields a huge, possibly infinite, deduction tree, giving rise to exponentially many abductive explanations. We suggest that a proof planning approach can structure the task of correcting a formula in such a way as to allow significant automation, while dramatically restricting the search space.     

Middle-out reasoning for synthesis and induction

We develop two applications of middle-out reasoning in inductive proofs: logic program synthesis and the selection of induction schemes. Middle-out reasoning as part of proof planning was first suggested by Bundy et al. Middle-out reasoning uses variables to represent unknown terms and formulae. Unification instantiates the variables in the subsequent planning, while proof planning provides the necessary search control. Middle-out reasoning is used for synthesis by planning the verification of an unknown logic program: The program body is represented with a meta-variable. The planning results both in an instantiation of the program body and a plan for the verification of that program. If the plan executes successfully, the synthesized program is partially correct and complete. Middle-out reasoning is also used to select induction schemes. Finding an appropriate induction scheme during synthesis is difficult because the recursion of the program, which is unknown at the outset, determines the induction in the proof. In middle-out induction, we set up a schematic step case by representing the constructors that are applied to induction variables with meta-variables. Once the step case is complete, the instantiated variables correspond to an induction appropriate to the recursion of the program. We have implemented these techniques as an extension of the proof planning system CL ^A M, called Periwinkle, and synthesized a variaety of programs fully automatically. Supported by the Swiss National Science Foundation and ARC Project BC/DAAD Grant 438. The work described in this paper was carried out while the first author was at the Department of Artificial Intelligence of the University of Edinburgh. Supported by the German Ministry for Research and Technology (BMFT) under grant ITS 9102 and ARC Project BC/DAAD Grant 438. Responsibility for the contents of this publication lies with the authors. Supported by SERC grant GR/J/80702, ESPRIT BRP grant 6810, ESPRIT BRP grant EC-US 019-76094, and ARC Project BC/DAAD Grant 438.     

Memoization-Based Proof Search in LF: An Experimental Evaluation of a Prototype

Elf is a general meta-language for the specification and implementation of logical systems in the style of the logical framework LF. Proof search in this framework is based on the operational semantics of logic programming. In this paper, we discuss experiments with a prototype for memoization-based proof search for Elf programs. We compare the performance of memoization-based proof search, depth-first search and iterative deepening search using two applications: 1) Bi-directional type-checker with subtyping and intersection types 2) Parsing of formulas into higher-order abstract syntax. These experiments indicate that memoization-based proof search is a practical and overall more efficient alternative to depth-first and iterative deepening search.     

Experiments with proof plans for induction

The technique of proof plans is explained. This technique is used to guide automatic inference in order to avoid a combinatorial explosion. Empirical research is described to test this technique in the domain of theorem proving by mathematical induction. Heuristics, adapted from the work of Boyer and Moore, have been implemented as Prolog programs, called tactics, and used to guide an inductive proof checker, Oyster. These tactics have been partially specified in a meta-logic, and the plan formation program, CLAM, has been used to reason with these specifications and form plans. These plans are then executed by running their associated tactics and, hence, performing an Oyster proof. Results are presented of the use of this technique on a number of standard theorems from the literature. Searching in the planning space is shown to be considerably cheaper than searching directly in Oyster's search space. The success rate on the standard theorems is high.     

一致性规划中互斥常量合成方法研究

为压缩一致性规划的状态空间,并加快一致性规划的求解速度,将常量引入到一致性规划中,定义一致性规划中的常量,形成新的知识表示“多值一致性规划任务”,定义多值一致性规划动作模型,提出一致性规划常量合成方法,给出一致性规划常量合成算法.该方法利用常量的特性在所有初始世界状态和所有实例动作中猜测、验证常量.理论分析和实验结果表明该算法能合成正确的一致性规划常量,生成多值一致性规划任务.为说明一致性规划常量的应用效果,把生成的多值一致性规划任务与规划解重用启发式结合求一致性规划解,并与规划系统CFF进行对比实验.实验结果表明求解质量和效率较高.     

Study on the Configuration Space Based Algorithmic Path Planning of Industrial Robots in an Unstructured Congested Three-Dimensional Space: An Approach Using Visibility Map

Obstacle avoidance and subsequently collision-free path planning is a potential field of robotics research, specially in the perspective of today's industrial scenario. In this paper, the celebrated method, namely, Visibility Map is being used to generate feasible collision-free near-optimal safe path(s) for a three- dimensional congested robot workspace using heuristic algorithms. The final path is obtainable in terms of joint configurations, by considering the Configuration Space of the task-space. The developed algorithms have been verified by considering typical 2D workspaces at the onset, cluttered with different obstacles (convex and/or concave) with regular geometries and later on, with the real spatial manifold. The outcome of these algorithms has been found instrumental in programming an industrial robot in order to perform a series of task in the shop-floor. A case-study reveals the effectiveness of the heuristics involved in the developed algorithms, by virtue of the successful application in an unstructured industrial environment to carry out robotized material handling operation in real-time.     

A privacy-preserving model for multi-agent propositional planning

Abstract

Over the last years, the planning community has formalised several models and approaches to multi-agent (MA) propositional planning. One of the main motivations in MA planning is that some or all agents have private knowledge that cannot be communicated to other agents during the planning process and the plan execution. We argue that the existing models of the multi-agent planning task do not maintain the agents’ privacy when a (strict) subset of the involved agents share confidential knowledge, or when the identity/existence of at least one agent is confidential. In this paper, first we propose a model of the MA-planning tasks that preserves the privacy of the involved agents when this happens. Then we investigate an algorithm based on best first search for our model that uses some new heuristics providing a trade-off between accuracy and agents’ privacy. Finally, an experimental study compares the effectiveness of using the proposed heuristics.     

A Collaborative Approach for Multi-Threaded SAT Solving

The last decade progresses have led the Satisfiability Problem (sat) to be a great and competitive practical approach to solve a wide range of industrial and academic problems. Thanks to these progresses, the size and difficulty of the sat instances has grown significantly. Among the recent solvers, a few are parallel and most of them use the message passing paradigm. In a previous work by Vander-Swalmen et al. (IWOMP, 146–157, 2008), we presented a fine grain parallel sat solver designed for shared memory using OpenMP and named mtss, for Multi Threaded Sat Solver. mtss extends the “guiding path” notion and uses a collaborative approach where a rich thread is in charge of the search-tree evaluation and where a set of poor threads yield logical or heuristics information to simplify the rich task. In this paper, we extend the poor thread abilities of mtss and present extensive comparative results on random 3-sat problems. These new experimentations show that fine grained techniques associated to poor tasks within the framework of mtss can achieve very interesting speedup on multi-core processors.     

Application of parallelized analogical planning to engineering design

Analogical planning provides a means of solving engineering problems where other machine learning methods fail. Unlike many machine learning paradigms, analogy does not require numerous previous examples or a rich domain theory. Instead, analogical planners adapt knowledge of solved problems in similar domains to the current problem. Unfortunately, the analogical planning task is an expensive one. While the process of forming correspondences between a known problem and a new problem is complex, the problem of selecting a base case for the analogy is virtually intractable.This paper addresses the issue of efficiently forming analogical plans. The Anagram planning system is described, which takes advantage of the massively parallel architecture of the Connection Machine to perform base selection and map formation. Anagram provides a tractable solution to analogical planning, with a complexity that is sublinear in the size of the plans.This paper describes the Anagram system and its parallel algorithms. The paper also presents theoretical analyses and empirical results of testing the system on a large database of plans from the domain of automatic programming.     

Hierarchical Path Search with Partial Materialization of Costs for a Smart Wheelchair

In this paper, the off-line path planner module of a smart wheelchair aided navigation system is described. Environmental information is structured into a hierarchical graph (H-graph) and used either by the user interface or the path planner module. This information structure facilitates efficient path search and easier information access and retrieval. Special path planning issues like planning between floors of a building (vertical path planning) are also viewed. The H-graph proposed is modelled by a tree. The hierarchy of abstractions contained in the tree has several levels of detail. Each abstraction level is a graph whose nodes can represent other graphs in a deeper level of the hierarchy. Path planning is performed using a path skeleton which is built from the deepest abstraction levels of the hierarchy to the most upper levels and completed in the last step of the algorithm. In order not to lose accuracy in the path skeleton generation and speed up the search, a set of optimal subpaths are previously stored in some nodes of the H-graph (path costs are partially materialized). Finally, some experimental results are showed and compared to traditional heuristic search algorithms used in robot path planning.     

An approach to automatic deductive synthesis of functional programs

The work deals with automatic deductive synthesis of functional programs. Formal specification of a program is taken as a mathematical existence theorem and while proving it, we derive a program and simultaneously prove that this program corresponds to given specification. Several problems have to be resolved for automatic synthesis: the choice of synthesis rules that allows us to derive the basic constructions of a functional program, order of rule application and choice of a particular induction rule. The method proposed here is based on the deductive tableau method. The basic method gives rules for functional program construction. To determine the proof strategy we use some external heuristics, including rippling. And for the induction hypothesis formation the combination of rippling and the deductive tableau method became very useful. The proposed techniques are implemented in the system ALISA (Automatic Lisp Synthesizer) and used for automatic synthesis of several functions in the Lisp language. The work has been partially supported by RFBR grant 05-01-00948a.     

A proof procedure for the logic of hereditary Harrop formulas

A proof procedure is presented for a class of formulas in intuitionistic logic. These formulas are the so-calledgoal formulas in the theory of hereditary Harrop formulas. Proof search in intuitionistic logic is complicated by the nonexistence of a Herbrand-like theorem for this logic: formulas cannot in general be preprocessed into a form such as the clausal form, and the construction of a proof is often sensitive to the order in which the connectives and quantifiers are analyzed. An interesting aspect of the formulas we consider here is that this analysis can be carried out in a relatively controlled manner in their context. In particular, the task of finding a proof can be reduced to one of demonstrating that a formula follows from a set of assumptions, with the next step in this process being determined by the structure of the conclusion formula. An acceptable implementation of this observation must utilize unification. However, since our formulas may contain universal and existential quantifiers in mixed order, care must be exercised to ensure the correctness of unification. One way of realizing this requirement involves labelling constants and variables and then using these labels to constrain unification. This form of unification is presented and used in a proof procedure for goal formulas in a first-order version of hereditary Harrop formulas. Modifications to this procedure for the relevant formulas in a higher-order logic are also described. The proof procedure that we present has a practical value in that it provides the basis for an implementation of the logic programming language Prolog.     

The Use of Proof Planning for Co-operative Theorem Proving

We describebarnacle: a co-operative interface to theclaminductive theorem proving system. For the foreseeable future, there will be theorems which cannot be proved completely automatically, so the ability to allow human intervention is desirable; for this intervention to be productive the problem of orienting the user in the proof attempt must be overcome. There are many semi-automatic theorem provers: we call our style of theorem provingco-operative, in that the skills of both human and automaton are used each to their best advantage, and used together may find a proof where other methods fail. The co-operative nature of thebarnacleinterface is made possible by the proof planning technique underpinningclam. Our claim is that proof planning makes new kinds of user interaction possible.Proof planning is a technique for guiding the search for a proof in automatic theorem proving. Common patterns of reasoning in proofs are identified and represented computationally as proof plans, which can then be used to guide the search for proofs of new conjectures. We have harnessed the explanatory power of proof planning to enable the user to understand where the automatic prover got to and why it is stuck. A user can analyse the failed proof in terms ofclam's specification language, and hence override the prover to force or prevent the application of a tactic, or discover a proof patch. This patch might be to apply further rules or tactics to bridge the gap between the effects of previous tactics and the preconditions needed by a currently inapplicable tactic.     

Decision Planning Knowledge Representation Framework: A Case-Study

This paper discusses experiences and perspectives of utilisation of declarative knowledge structures as a convenient knowledge base medium in configuration expert systems. Although many successful systems have been developed, these are often difficult to maintain and to generalize in rapidly changing domains. In this paper we address the problem of building intelligent knowledge based systems with emphasis on their maintainability. Firstly, several industrial applications of proof planning, a theorem proving technique, will be described and their advantages and flaws will be discussed. This discussion is followed by the theoretical foundation of decision planning knowledge representation framework that, based on proof planning, facilitates separate administration of inference problem solving knowledge and the domain theory axioms. Machine learning methods for maintaining the inference knowledge to be up-to-date with permanently changing domain theory are commented and evaluated.     

Proof planning with multiple strategies

Proof planning is a technique for theorem proving which replaces the ultra-efficient but blind search of classical theorem proving systems by an informed knowledge-based planning process that employs mathematical knowledge at a human-oriented level of abstraction. Standard proof planning uses methods as operators and control rules to find an abstract proof plan which can be expanded (using tactics) down to the level of the underlying logic calculus.In this paper, we propose more flexible refinements and a modification of the proof planner with an additional strategic level of control above the previous proof planning control. This strategic control guides the cooperation of the problem solving strategies by meta-reasoning.We present a general framework for proof planning with multiple strategies and describe its implementation in the Multi system. The benefits are illustrated by several large case studies, which significantly push the limits of what can be achieved by a machine today.     

Nonsmooth µ‐synthesis

We revisit robust complex‐ and mixed‐ µ‐synthesis problems based on upper bounds and show that they can be recast as specially structured controller design programs. The proposed reformulations suggest a streamlined handling of µ‐synthesis problems using recently developed (local) nonsmooth optimization methods, where both scalings or multipliers and a controller of given structure are obtained simultaneously. A first cut of the nonsmooth programming software for structured H_∞ synthesis is made available through the MATLAB R2010b Prerelease, Robust Control Toolbox Version 3.5 developed by The MathWorks, Inc. Copyright © 2010 John Wiley & Sons, Ltd.     

Planning as Propositional CSP: From Walksat to Local Search Techniques for Action Graphs

Graphplan-style of planning can be formulated as an incremental propositional CSP where the (boolean) variables correspond to operator instantiations (actions) that are or are not scheduled at certain time steps. In this paper we present a framework for solving this class of propositional CSPs using local search in planning graphs. The search space consists of particular subgraphs of a planning graph corresponding to (complete) variable assignments, and representing partial plans. The operators for moving from one search state to the next one are graph modifications corresponding to revisions of the current variable assignment (partial plan), or to an extension of the represented CSP.Our techniques are implemented in a planner called LPG using various types of heuristics based on a parametrized objective function, where the parameters weight different constraint violations, and are dynamically evaluated using Lagrange multipliers. LPG's basic heuristic was inspired by Walksat, which in Kautz and Selman's Blackbox can be used to solve the SAT-encoding of a planning graph. An advantage of LPG is that its heuristics exploit the structure of the planning graph, while Blackbox relies on general heuristics for SAT-problems, and requires the translation of the planning graph into propositional clauses. Another major difference is that LPG can handle action execution costs to produce good quality plans. This is achieved by an anytime process minimizing an objective function based on the number of constraint violations in a plan and on its overall cost. Experimental results illustrate the efficiency of our approach, showing, in particular, that LPG is significantly faster than Blackbox and other planners based on planning graphs.