Writing dependently typed functional programs that capture non-trivial program properties is difficult in current systems due to lack of proof automation. We identify proof patterns that occur when programming with dependent types and detail how automating such patterns allow us to work more comfortably with types that capture, for example, membership, ordering and non-linear arithmetic properties. We describe the role of the rippling heuristic, both for inductive and non-inductive proofs, and generalisation in providing such automation. We then discuss an implementation of our ideas in Coq with practical examples of dependently typed programs, that capture useful program properties, which can be verified automatically. We demonstrate that our proof automation is generic in that it can provide support for working with theorems involving user-defined functions and inductive data types.

This paper presents an action selection method using fuzzy logic. The objective is to solve behaviour conflict in behaviour-based architectures for virtual agent navigation in unknown virtual environments. Two main problems have been identified: how to decide which behaviour should be activated at each instant; and how to combine the results from different behaviours into one action. The method uses fuzzy α-levels to compute behaviour weight for each behaviour and the final action is selected using the Huwicz criterion. The results clearly demonstrate the mapping of inputs to output with a near-optimum path in every navigation task.

In this paper we show that the automated reasoning technique of deductive synthesis can be applied to address the problem of machine-assisted composition of e-Science workflows according to users' specifications. We encode formal specifications of e-Science data, services and workflows, constructed from their descriptions, in the generic theorem prover Isabelle. Workflows meeting this specification are then synthesised as a side-effect of proving that these specifications can be met.

The local search algorithm WSat is one of the most successful algorithms for solving the satisfiability (SAT) problem. It is notably effective at solving hard Random 3-SAT instances near the so-called `satisfiability threshold', but still shows a peak in search cost near the threshold and large variations in cost over different instances. We make a number of significant contributions to the analysis of WSat on high-cost random instances, using the recently-introduced concept of the backbone of a SAT instance. The backbone is the set of literals which are entailed by an instance. We find that the number of solutions predicts the cost well for small-backbone instances but is much less relevant for the large-backbone instances which appear near the threshold and dominate in the overconstrained region. We show a very strong correlation between search cost and the Hamming distance to the nearest solution early in WSat's search. This pattern leads us to introduce a measure of the backbone fragility of an instance, which indicates how persistent the backbone is as clauses are removed. We propose that high-cost random instances for local search are those with very large backbones which are also backbone-fragile. We suggest that the decay in cost beyond the satisfiability threshold is due to increasing backbone robustness (the opposite of backbone fragility). Our hypothesis makes three correct predictions. First, that the backbone robustness of an instance is negatively correlated with the local search cost when other factors are controlled for. Second, that backbone-minimal instances (which are 3-SAT instances altered so as to be more backbone-fragile) are unusually hard for WSat. Third, that the clauses most often unsatisfied during search are those whose deletion has the most effect on the backbone. In understanding the pathologies of local search methods, we hope to contribute to the development of new and better techniques.

We describe a proof plan that characterises a family of proofs corresponding to the synthesis of recursive functional programs. This plan provides a significant degree of automation in the construction of recursive programs from specifications, together with correctness proofs. This plan makes use of meta-variables to allow successive refinement of the identity of unknowns, and so allows the program and the proof to be developed hand in hand. We illustrate the plan with parts of a substantial example-the synthesis of a unification algorithm.