Research

Constraint Programming, Search & Symmetry, University of Huddersfield
From October 2001 -
This is my current research at the University of Huddersfield, where I am studying for a Ph D. in Artifical Intellegence.

Maple-PVS interface, University of St Andrews
June 2001 - Sept 2001
I worked as graduate researcher on this project, last summer.

GAP (Groups and Algorithmic Programming), University of St Andrews
June 2000 - May 2001
I started working with GAP during the summer of 2000, where I wrote a new random number generator for the system. I then carried on this work to become my Senior Honours project, where I wrote a statistical library for GAP.

Constraint Programming, Search & Symmetry

This is an EPSRC sponsered project. The project outline written for the EPSRC before the project started is below, I am the Ph d. student mentioned!:

Constraint problems, in which there are explicit constraints on the possible solutions, arise in many practical contexts. In general, such problems are NP-complete, yet their effective solution is of enormous industrial and commercial importance. They are typically solved using AI search techniques, in Constraint Programming software packages such as ILOG Solver and Eclipse. Symmetry may be inherent in the problem, or may arise through modelling it as a constraint problem. In either case, symmetry can lead to redundant search, where many symmetrically equivalent blind alleys are explored wastefully. To avoid this, symmetry-breaking constraints can be added, to exclude all but one of each equivalence class of solutions. Recently, a systematic and general method has been introduced for doing this while search is in progress [1,2]. This requires the effect of each symmetry to be described and has been shown to be extremely effective where the number of symmetries is reasonably small (up to a few thousands). In many cases, however, the number of symmetries is far too large to allow them to be specified individually. The project will develop ways of dealing with this situation, by reasoning about the symmetry group as a whole, using group theory.

The RA at St Andrews will use the computational algebra system GAP and explore its integration with a constraint programming system to handle highly symmetric problems. The PhD student will make use of the ideas developed at St Andrews and develop practical approaches to solving problems in sports scheduling [3], balanced incomplete block design [4] and other combinatorial design problems. A focus will be on how to choose a subset of the symmetries, of manageable size, whose elimination will exclude most of the symmetrically equivalent solutions. Although informed by theory, it is envisaged that the emphasis will be investigative and empirical.

References

[1] R. Backofen and S. Will. Excluding symmetries in constraint-based search. In Proceedings CP'99, Springer, LNCS 1713, 1999.

[2] I. P. Gent and B. M. Smith. Symmetry breaking in constraint programming. In Proceedings ECAI'2000, ed. W. Horn, pp. 599-603, 2000.

[3] J.-C. Regin. Minimization of the number of breaks in sports scheduling problems using constraint programming. In Constraint Programming and Large Scale Discrete Optimization, Proceedings of the DIMACS Workshop, 1998. Eds. E.C. Freuder and R.J. Wallace, 2001.

[4] P. Meseguer and C. Torras. Solving strategies for highly symmetric CSPs. In Proceedings IJCAI'99, pp. 400-405, 1999.


People involved with this Project



Maple-PVS Interface

Aims and Objectives

The aim of this project is to allow users of the Maple computer algebra system to solve problems which require theorem proving technology, without the need to interact with a theorem prover directly. In fact, in one idealised scenario the user might not know that a theorem prover is being used at all. However, there are also situations where an experienced user may wish, or need, to guide the theorem prover through difficult proof attempts.

Although we have chosen to work with Maple for this project, alternative systems such as AXIOM or Mathematica are not ruled out. The choice of PVS as the theorem prover is more important to us and was motivated by our work on real analysis in PVS.

Background

The project is in its early stages and it is too soon to describe it in great detail. However, we have already developed a system to enable the interactive, LISP-based PVS application to be used more easily as a blackbox which has been well received by PVS developers. Using this system we have created a small Tcl/Tk application (pvs-ctl) which provides a low-level alternative to the standard Emacs interface to PVS: this application forms the basis of our Maple/PVS prototype. We have also developed a small library of C functions to allow Maple 6 worksheets to launch PVS as a child process and communicate with it.

Architecture

Our Maple/PVS prototype is a loosely-coupled, master-slave system in which Maple 6 is the master and pvs-ctl, our Tcl/Tk application, is the slave. Commands from Maple 6 are accepted by pvs-ctl and passed onto PVS. Output from PVS is translated by a small lexical analyser (pvs-filter) that we have developed to simplify the semantic analysis of PVS output. Useful PVS messages are given to Maple while extraneous data is filtered by Tcl/Tk and displayed to the user.

It is important not to send all PVS output to Maple since most of it is irrelevent to the Maple/PVS computations and it is intended to keep the PVS/Emacs user informed of the current proof state and progress. If Maple had to filter messages, deal with PVS questions and interact with the user on behalf of PVS, it would significantly complicate the Maple/PVS protocol. Indeed we would have to re-implement most of the PVS/Emacs LISP interface in C or Maple to achieve this. At the other extreme, we cannot discard information that is not relevent to Maple: some of it may be important to the user and provide indications of progress. It is this kind of data that is displayed by pvs-ctl.

The prototype Maple/PVS is structured as follows:

As with many prototypes, life is not quite so simple: any system containing two different interactive applications, communicating without user-interaction, is likely to suffer from deadlocks. Even with the most careful planning, Maple 6 may send a query to PVS and be waiting for the reply. Meanwhile PVS responds with a question and is waiting for its reply. In such situations the user must provide PVS with the answer to its question.

For this reason, the Tcl/Tk application displays the prover commands, responses and information messages that are normally seen by a PVS/Emacs user. It also provides a text-entry field in which PVS commands can be typed in response to PVS questions. At present the Tcl/Tk interface allows us to resolve deadlocks but in the future it may also provide a way for experienced PVS users to guide PVS through difficult proof attempts.

The Tcl/Tk Interface To PVS

Below is an early screen-shot of pvs-ctl in action:

This prototype uses red to highlight PVS responses (filtered by pvs-filter) that have not been programmed for: at the start we have a buffer message (SB) followed by a request to evaluate a LISP expression (XE). The green Q.E.D. is sent back to Maple and indicates that the proof attempt was successful: in this instance that the function f(x) = x+1 is continuous at x=3 where f(x) is a function over the real numbers. Yellow is used to highlight the PVS prompts which are also sent to Maple so that it knows when PVS has completed one command and is ready for the next. The status-bar at the bottom of the window displays the same messages as the status-bar at the bottom of a typical PVS/Emacs session, while the faint box in the bottom-right corner flashes red when PVS is garbage collecting!

People I worked with on this project

My involvment in the project

I spent two months writing (and proving) some PVS functions to prove continuity and differentiablity, that colud be used in Maple via the interface. These functions have been tested to be(due to the nature of PVS) more reliable than the built in Maple versions.


GAP

GAP (Groups, Algorithms and Programming) is a system for computational discrete algebra with particular emphasis on, but not restricted to computational group theory. GAP was developed at Lehrstuhl D für Mathematik (LDFM), RWTH Aachen, Germany from 1986 to 1997. After the retirement of J. Neubüser from the chair of LDFM, the development and maintenance of GAP is coordinated by the School of Mathematical and Computational Sciences at the University of St. Andrews, Scotland. Several users have contributed to the system via share packages which can be used in the same form as the main library. There are presently two versions in distribution:
  • Version 4 .2 (GAP 4r2), incorporates several new basic features developed over the last years. In particular it provides much improved possibilities for defining mathematical structures of your own special interest.
  • Version 3.4, patchlevel 4, (GAP 3.4.4) released April 1997 is still available as some of its features and share packages are not yet available for GAP 4. However it is not developed further any longer.
More information about Gap can be found at http://www-gap.dcs.st-and.ac.uk/~gap/

People involved with this Project

[ Home | Research | Publications |Teaching |Friends|Interests| Contact Details ]

Maintained by : K. E. Petrie