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
Programme:
| 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 |
Abstracts
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.
Directions:
The KB (King's Buildings) site is about 2.5 miles south of the
Edinburgh centre. See
http://www.dcs.ed.ac.uk/maps/Edinburgh.ps
for a map showing the streets between the city centre and KB and
http://www.ed.ac.uk/graphics/maps/kb.gif
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.
