Research Abstracts - 2006

Verifying Abstract Plans With a Theorem Prover

Harold Fox

Introduction

The traditional planning problem has been to take a start state, a goal state, and a set of actions, and produce a sequence of actions that will take the start to the goal. The most recent work has focused on the problem of planning under uncertainty, where the produced plan must have branches and contingencies that are chosen based on observations not known at planning time. I am considering a similar problem: how to construct a plan where the actions are deterministic, but the start and goal states are unknown. All I know is that the start and goal states will satisfy some higher-order predicate. I call such a plan an abstract plan. This problem is very similar to the task of program synthesis, the construction of executable computer code from a high-level logical specification of what the code ought to do.

For a system to correctly search for an abstract plan, it must first be able to verify that any given plan was correct. That is, it must be able to check that if the start state satisfies one particular predicate and the goal state satisfies another, it can verify that the sequence of steps produced by the plan will be correct in all circumstances. This is the problem I have been considering recently.

This plan verification task overlaps considerably with the formal verification of software systems. However, it has some critical differences. For example, most recent research in software verification systems is concerned with validating only one particular property of the system, such as whether it terminates or causes a run-time error, in a large body of code. In contrast, validating an abstract plan means checking that the plan meets the specification fully. Thus, it consists of constructing a complete, formal proof that the plan is correct. A second major difference is that the logic of an abstract plan can be different from that of a programming language. Because the plan is automatically generated, it can have the most convenient representation I can make.

This logical freedom means that I can choose an abstract plan representation that is a useful mid-point between the flexibiliity of a programming language and the verifiability of a formal, logical proof language. In particular, I can avoid temporal logic, and I can ensure that every recursive function correctly breaks down into its base and reducing components.

The AireProve language and theorem prover

As our first major step, we have developed the AireProve proof language and theorem prover [1]. This is an intuitive language for writing proofs in higher-order logic. It is different from standard higher order theorem provers such as Isabelle or Coq [2][3], because it does not use types. This makes the language simple to write and understand. The syntax uses Scheme-like expressions with a block structure for defining theorems and proofs. The proof checking uses a combination of a rewrite rule engine and a first-order resolution search.

The language interpreter parses the document and produces a sequence of proof problems that are passed to the underlying prover. Each proof problem consists of a fact to prove and a set of hypotheses. The hypotheses and the negation of the fact are converted into a list of or-and trees, and the prover attempts to find a contradiction.

The resolution search performs first-order resolution on matching trees, continually adding new trees to its list. When it finds a new set of singleton trees without ors, it adds the singleton's data as a new rewrite rule to the rewrite rule engine. This expression matching engine does a bounded depth first search using all of the rewrite rules recursively to try to match the hypotheses to the T truth literal.

In our initial experiments, we have used AireProve to prove the Knaster-Tarski fixed-point theorem, which states that for any complete lattice L and any funcction f:L -> L, there is a point x in L for which f(x) = x. We have also proven, using the induction hypothesis, that a large class of recursive functions exist and are well-defined. From this, we have proven that for any recursive definition, a well defined recursive function can be created that evaluates correctly on arguments that reduce to a base case, and that evaluates to BOTTOM everywhere else.

References:

[1] Harold Fox. AireProve: A New Proof Language and Theorem Prover. CSAIL Technical Report.

[2] Lawrence C. Paulson. The Isabelle Reference Manual.

[3] Bruno Barras, Samuel Boutin, et al. The Coq Proof Assistant Reference Manual.