ARW 5 Statements of Research Interests.

 

  • Richard Boulton, University of Edinburgh
    My research interests within automated reasoning include proof planning, mathematical induction, higher-order logic, decision procedures, and interactive theorem proving. I am also interested in mechanized support for reasoning about computer languages, formal hardware verification, hardware description languages, and functional programming.

  • Alan Bundy, University of Edinburgh
    I am interested in a wide range of different aspects of automated reasoning. The following describes projects in my research group with which I am involved.

    Proof Planning: We have pioneered the use of proof planning as a global strategy for guiding reasoning. Recent work has focussed on the use of critics for patching failed proof attempts. We are testing the generality and robustness of proof planning by linking our clam proof planner to Mike Gordon's hol theorem prover.

    Inductive Proof: Most of our work has been on guiding proofs by mathematical induction using proof plans. For instance, we are investigating heuristics for selecting induction rules. A lot of our current effort is focussed on extending heuristic techniques originally devised for first-order logic to higher-order.

    Rippling: A lot of our effort has focussed on the {\e rippling method, which tries to reduce the difference between induction conclusion and induction hypothesis. We have adapted rippling to reasoning about conjunctions of relations as in logic programs and some hardware verification proofs. We are also looking at rippling in a higher-order context.

    Formal Methods: We have applied this work to the verification, synthesis and transformation of software and hardware. Recent work has focussed on hardware verification, functional program synthesis, verifying concurrent systems using CCS and proving properties of lazy lists using coinduction. We are just starting to look at VDM proof obligations.

    Program Editor: We are applying techniques of program synthesis to the construction of an editor for ML programs, which supports programming by analogy and guarantees well-definedness and termination.

    Other Mathematics: We have also looked at summing series and limit theorems, especially at the role of rippling in these proofs.

    Cooperative Problem Solving: We are using proof planning to provide a high-level language for improving interactive theorem provers.

    Informal Reasoning: We are investigating how reasoning with diagrams can be automated, using the constructive omega rule.

    Concept Formation: We are automating the formation of group theoretic concepts. The value of concepts is assessed on a multi-dimensional scale according to their ability to classify finite groups.

    Configuration: We have applied proof planning to the configuration of computer systems and air compressors.

    Bridge: We have also applied proof planning to the game of bridge, including declarer play, bidding, drawing inferences and tutor systems. We recently had a project on Go.

    Uncertainty: We have developed a logic for reasoning under uncertainty called incidence calculus. Sets of possible worlds are associated with formulae, instead of numbers. Upper and lower numeric bounds can be calculated from these possible worlds. This arrangement enables incidence calculus to reason with dependent information, which is not possible with purely numeric uncertainty logics.

  • Michael Fisher, Manchester Metropolitan University
    and Andrew Ireland, Heriot-Watt University - Multi-Agent Proof-Planning
    Reasoning using induction is a key aspect of proof in higher-order logics, yet is inherently complex. In this context, the notion of proof planning has been found to be useful, providing high-level guidance through inductive proofs. While this approach has been successfully applied within, for example, the Oyster/CLAM system, proof planning is itself difficult. The search space considered is large, and the planning and patching operations may be arbitrarily complex.

    Often, in the case of large search spaces, parallel techniques may be applied. However, while parallelisation is particularly effective when independent components can be identified, such techniques are less successful if all the elements are tightly coupled and interacting. In recent years, agent-based systems have been increasingly used to attack such complex problem spaces, for example via competitive and cooperative search.

    Thus, the primary aim in this work is to apply novel approaches from the area of agent-based systems to the development of improved proof planning systems. In particular, by viewing a proof as being distributed amongst autonomous agents, we may be able to combine the benefits of parallel search in large problem spaces, with agent-based aspects in complex problem spaces.

    Our long term aim is to incorporate, within a variety of communicating autonomous agents, not only effective control and organisational strategies, but also AI techniques such as learning and analogy. This leads to the possibility of developing agent societies capable of supporting proof planning. Such societies would evolve, adapt and organise themselves in order to attack the particular problem under consideration.

    [For a copy of the draft paper, email either of the authors Michael Fisher or Andrew Ireland.]

  • Alan M. Frisch, University of York
    and Timothy J. Peugniez - Solving Non-Boolean Satisfiability Problems with Local Search

    Much excitement has been generated by the recent success of stochastic local search procedures at finding satisfying assignments to large sets of formulas of propositional logic. These procedures use hill-climbing methods to search a space of all assignments for one that satisfies the given set of formulas. The problem of finding a satisfying assignment can be seen as a special case of a constraint satisfaction problem in which every variable has a domain of two values and the constraints are represented as propositional formulas (often clauses). However, in many naturally-arising constraint satisfaction problems domains are non-Boolean---that is, they contain more than two values.

    The typical way to solve non-Boolean problems by local search is to map them to Boolean problems that use multiple Boolean variables in place of each non-Boolean variable and then use one of the Boolean local search procedures. In particular, a non-Boolean problem containing a variable X with domain d1, ..., dn is mapped to a Boolean problem containing n Boolean variables, X1, ..., Xn. The idea is that a Boolean assignment maps Xi to true if and only if the corresponding non-Boolean assignment maps X to di. However, one must add additional formulas to the Boolean representation to represent the constraint that a satisfying assignment must satisfy exactly one of X1, ..., Xn. Though the "at least one" constraint for a variable can be expressed by a single clause, the number of "at most one" clauses grows quadratically with n, the domain size.

    Our work proposes and investigates solving non-Boolean satisfaction problems directly by searching through a space of assignments to the original non-Boolean variables. In particular, we have generalised Walksat, a highly-successful local-search procedure for Boolean satisfiability problems, to work on problems with domains of arbitrary size.

    Our experiments show that our non-Boolean version of Walksat, called NB-Walksat, outperforms the original Walksat on randomly-generated, non-Boolean problems near the phase transition. One reason for this is that with larger domain sizes Walksat must maintain a large number of "at-most-one" clauses, which significantly increases the time it takes to move from one assignment to another. Furthermore, the Walksat search space only contains assignments that satisfy the "exactly-one" constraints, whereas the Walksat search space also contains assignments that violate these constraints. Though some researchers had suspected that these extra assignments would provide a shorter path to the solution, our experiments show that the effect is just the opposite. Consequently, even on graph-colouring problems, which do not require the "at most one" clauses, NB-Walksat outperforms Walksat.

  • Ian Green, University of Edinburgh
    Program synthesis by automating proof by mathematical induciton in constructive logics. Currently looking at the generalization of the `rippling' proof method to higher-order logics, and at constructing well-founded orders.

  • Anthony McIsaac, SGS-Thomson Microelectronics Limited
    Application of formal reasoning to microprocessor and system design. Systematic use of modelling and abstraction techniques to reduce problems to tasks that can be handled by automated tools.

  • Manfred Kerber, University of Birmingham
    My research interests are mainly focussed on interactive theorem proving with mathematical applications. They can be roughly subdivided into the fields proof planning, problem reformulation, and formalisation of partiality. In the areas of proof planning and problem reformulation I am interested in applying human oriented techniques to mechanical theorem proving. I am in particular interested in the adaptation process of problems either by reformulating the original problem or adapting a related proof plan. My interest in partiality is motivated by the need for a correct treatment of expressions like 1/0.

  • Alan Smaill, University of Edinburgh

    Constructive logic and automation of constructive reasoning; program synthesis.