The Scottish Theorem Proving seminar series

Friday 13th February 1998

Lecture Theatre C
James Clerk Maxwell Building
King's Buildings
University of Edinburgh

14:00 - 17:00


14:00: Welcome
14:10-14:40: "Can Diagrammatic Reasoning be Automated?"
Mateja Jamnik
Artificial Intelligence, Edinburgh
14:50-15:20: "Practical Semi-Automated Theorem Proving"
Helen Lowe
Computer Studies, Glasgow Caledonian
15:30-16:00: Tea, coffee and cold drinks.
16:00-16:30: "Phase Transitions, Constrainedness and Search"
Toby Walsh
Computer Science, Strathclyde
16:40: Close


Can Diagrammatic Reasoning be Automated?
Mateja Jamnik
Department of Artificial Intelligence
University of Edinburgh

Theorems in automated theorem proving are usually proved by formal logical proofs. However, there is a subset of problems which humans can prove by the use of geometric operations on diagrams, so called diagrammatic proofs. Insight is often more clearly perceived in these than in the corresponding algebraic proofs; they capture an intuitive notion of truthfulness that humans find easy to see and understand. We are investigating and automating such diagrammatic reasoning about mathematical theorems. The user gives the system, called DIAMOND, a theorem and then interactively proves particular concrete instances of it by the use of geometric operations on the diagram. These operations are the ``inference steps'' of the proof. DIAMOND then automatically induces from these proof instances a generalised schematic proof. The constructive omega-rule is used as a mathematical basis for such generalised schematic proofs. This approach allows us to embed the generality in the schematic proof so that operations need only be applied to concrete diagrams. We are investigating the translation of such schematic proofs into algebraic proofs as one route to confirm that the generalisation of the schematic proof from the proof instances is sound.

Practical Semi-Automated Theorem Proving
Helen Lowe
Computer Studies
Glasgow Caledonian University

Hitherto the basic choice of tool support for proof in formal methods has been between various interactive and automated systems. Interactive systems are generally difficult to use and automated systems are still limited in the range of theorems which they can prove truly unaided. A typical mode of interaction with an automatic theorem prover is a marathon effort involving interpreting screenfuls of text and spotting missing lemmas. While better interfaces help, they are not the whole answer. The middle ground between interactive and automated systems has not been fully exploited, the difficulty lying in determining how to divide the effort between human and automaton, and the content and form of information to be provided by each. Automating the use of a tactic-based theorem prover by means of proof planning provides a good starting point for bridging the gap.

Phase Transitions, Constrainedness and Search
Toby Walsh
Department of Computer Science
University of Strathclyde
(joint work with Ian Gent)

There has been much interest in threshold phenomena, so called "phase transitions", in a variety of different NP-complete problems including propositional satisfiability. Whilst random satisfiability problems are often very easy to solve, instances from around the phase boundary tend to be hard to solve. I will present a unifying framework for studying such phase transition phenomena. I will introduce a parameter that measures the ``constrainedness'' of search problems. This constrainedness parameter can be used to locate phase transitions in many different NP-complete problem classes. It can also be used in a heuristic to guide search.


The KB (King's Buildings) site is about 2.5 miles south of the Edinburgh centre. See

for a map showing the streets between the city centre and KB and

for a map of the KB site. James Clerk Maxwell is the largest building on the bottom (southernmost) side of the KB site map. Lecture Theatre C is at the end of the curved wing extending from the north side of the building. It's best to enter the building from one of the entry points marked on the map where the wing joins the main body of the building. After you go in, go up the flight of stairs you'll see in the foyer and turn right to reach Lecture Theatre C.

There are various busses you can catch from the centre of town near Waverley station to get to KB. The simplest is the #42. The fare is 65p one way (exact change only). The #46 will take you back again. To get to the #42 bus stop from Waverley, exit up one of the road ramps and turn left at the top. Walk along to the roundabout and turn right up the hill on Market St. Walk to the top of the Market St where it joins North Bank St and the bus-stop will be a few yards away on your right. During the day, the #42 should stop there at approx :03, :18, :33, and :48 past each hour. The journey takes about 15mins. Get off the bus at the stop marked on the map on Mayfield Rd, before the bus turns left to go down Esslemont Rd. Just before the stop the bus will have been going uphill for a while in a residential area. The stop for the #46 back into town is across the road from the #42 stop. Times for busses there are nominally :09, :24, :39, and :54 past each hour until 6:24, after which they run every half hour at :47 and :17 past.

If you come by bike, there are bike racks around the NW entrance to JCMB. If you come by car, it's best to park in one of the side streets off the KB site.

Return to Scottish Theorem Proving page.