Loading...
Please wait, while we are loading the content...
Similar Documents
Using Abstraction Interactively
| Content Provider | Semantic Scholar |
|---|---|
| Author | Sebastiani, Roberto Manzo, Mauro Di Giunchiglia, Fausto |
| Copyright Year | 2007 |
| Abstract | ion f belonging to such a set, for any ground theorem ', exists in 2 a proof 2 of the abstracted theorem f('); moreover exists (at least) one way to \map back" (at least one of the possible) 2 to 1 which gives rise to an outline of the ground proof. can be subsequently re ned. It is important to observe that in interactive abstract theorem proving there is no need to interact only with human beings. Thus, in order to achieve automatic theorem proving in limited domains, an interactive abstract theorem prover, like ABSFOL, could be interfaced with external control programs based on euristic strategies [Kno91, BGW91]. Moreover, such system can be provided with an internal ML-like metalanguage for writing programs which implements control strategies, called tactics [GT93]. Automated theorem proving can then be implemented by writing complex tactics. 3 The map colouring problem As an example of interactive abstract theorem proving, in this paper we will consider the very well-known problem of colouring the various regions of a planar map using only four di erent colours. In Figure 1 we nd a very simple example taken from [McC90]. According to McCarthy, we can formalize the problem in terms of theorem proving as follows. We need a set of variables (like Albania, Andorra, Austria, : : : or r1,r2, : : : ) each representing a region of the given map, a binary predicate n() \next", representing the frontier constraints (e.g. n(Austria,Italy)), and a set of the four individual constants y; b; g; r (yellow, blue, green, red). Then we de ne an axiom \colours", written as a conjunction of colouring constraints like n(y,b) (\a yellow-coloured state can border a blue-coloured one"). Using ABSFOL, the problem can be initialized as follows: 4 NONAME:: NAMECONTEXT gmap; GMAP:: DECLARE INDCONST y b g r; GMAP:: DECLARE INDVAR r1 r2 r3 r4 r5 r6; GMAP:: DECLARE PREDCONST n 2; GMAP:: AXIOM colours : n(y,b) and n(y,g) and n(y,r) and n(b,y) and n(b,g) and n(b,r) and n(g,y) and n(g,b) and n(g,r) and n(r,y) and n(r,b) and n(r,g); The goal is given by the conjuction of all and only the frontier constraints of the map: exists r1 ... r6. ( n(r1,r2) and n(r1,r3) and ... and n(r5,r6) ) 4In ABSFOL, Teletype font is used to write the input and output of ABSFOL. UPPERCASE TELETYPE is used for key-words. \::" is the ABSFOL prompt: the string before \:: " is the name of the current context, that is the theory we are working in. NAMECONTEXT names the current context. DECLARE adds new symbols to the current context. AXIOM adds an axiom to the current context. Both the input and the output have been slightly edited to make them more readable. 4 Figure 1: A solution to a map colouring problem via abstraction. Using a formalization like this, the solution is usually very computationally explosive for any automatic theorem prover [McC90], as it involves a lot of backtracking. According to Mozeti~c [Moz90], for a map of 32 European countries a prolog program implementing a chronological backtracking algorithm needs 12 CPU-time days. We want to show that abstraction can guide a theorem prover to solve the problem in linear time, eliminating any backtrack 5. Following Kempe [Kem79] we rst note that any region with three or fewer neighbours presents no problem, as there is always a colour available. Thus we can abstract the original map by eliminating all such countries (see Fig 1). In our formalization, this means mapping any frontier constraint involving such less-relevant countries (e.g. n(r3,r4)) into TRUE (step (ii)). This gives rise to a simpler representation of the problem, as the number of countries will have decreased and, most important, many of the countries left will surely loose some neighbours. Thus we can iterate this process until we have no region with more than three neighbours: this nal representation is automatically solvable at the rst attempt in linear time, without backtracking (step (iii)). Each level's solution becomes a plan for the next lower level (step (iv)), and can also be re ned without backtracking as it also needs colouring only less-thenfour-bordered regions (step (v)). We can use this process with complicate maps. For instance, we can colour a 1989 Europe map 6 using only three consequent abstractions. The rst abstraction introduces the greatest simpli cation of the problem, as it eliminates the following countries: Spain, Portugal, Andorra, Ireland, United Kingdom, Iceland, Norway, Sweden, Finland, Holland, Luxembourg, Lichtenstein, Denmark, Poland, Turkey, Monaco, 5Even if a very simple input problem is given, a standard algorithm for automatic theorem proving could need some backtracking to solve it [McC90]. For instance, if we try to colour the map in Figure 1 starting from countries r4,r5 by using an ordinary chronological backtracking algorithm, we will need more than 24 steps instead of 6. 6 In order to make comparisons with [Moz90], we refer to a 1989 Europe map, with still Czechoslovakia, Yugoslavia and two distinct german nations. 5 S.Marino, Vatican City, Albania, East Germany. As there are still some countries with more than three neighbours, we must iterate the process. The second and third abstraction remove respectivelyBelgium, Czechoslovakia, U.S.S.R., Bulgaria, Greece, and France, West Germany, Romania, Hungary. Now the abstract problem is su ciently reduced to be solved directly, as there are only four countries left: Switzerland, Italy, Austria, Yugoslavia. Now the whole colouring process follows easily, by colouring at each step all the nations of a di erent abstract level (in linear time). As a whole, three concatenated abstractions have guided the system to a complete colouring, with no backtracking. 4 The ve steps In this section we describe some of the details of the ve steps of interactive abstract theorem proving, as they are listed in the schema of Page 3. For such a task, we present a full mechanization of the map colouring example of Figure 1. 4.1 Step (i): abstraction de nition As we said in Section 2, in order to achieve satisfactorily an abstract-checked proof for a given goal ' in 1, the abstraction f : 1 ) 2 must be very speci c for '. For such a task ABSFOL provides some tools for de ning abstractions [Seb93]: a language, general enough to preserve all the expressive power of the formal de nition of abstraction [GW92a]; an interpreter for such a language, which allows for the automatic (partial or total) generation of the abstract space; a hardwired library of context-independent abstractions (abstraction prototypes), which can be instantiated into the desired application. In order to solve the map colouring problem of Figure 1, the user can de ne the abstraction kempe, which eliminates the regions r4 and r5 7: GMAP:: MAKECONTEXT amap; GMAP:: DEFINE ABSTRACTION kempe : gmap ==> amap BY PROTOTYPE logic_pres .... NEWRULESABS( n(r4,$x) ) := TRUE ABS( n($x,r4) ) := TRUE ABS( exists r4. $A ) := ABS($A) ABS( n(r5,$x) ) := TRUE ABS( n($x,r5) ) := TRUE ABS( exists r5. $A ) := ABS($A); 7 MAKECONTEXT creates a new empty context. gmap and amap are the names of the ground and abstract contexts. The symbols beginning with \$" are meta-variables. As ABSFOL is still at prototype level, the syntax of the commands can change from time to time. 6 An abstraction is de ned by a set of (terminating) rewrite rules, plus a description of the mapping of the alphabet symbols. The declaration of kempe can be easily performed by instantiating an abstraction prototype, that is a pre-compiled set of rules: \similar" abstractions are obtained from the same prototype. In particular logic pres consists of rules like: ABS(forall $x. $A) := forall $x. ABS($A) ABS($A and $B) := ABS($A) and ABS($B) which preserve the logical stucture of a w . We can note that it is easy to write an external program able to generate automatically the suitable abstraction for a given map colouring problem: finitialize abstraction f : 1 ) 2 g for any country ri do if fri occurs less then four times in the goalg then fadd to f the rules for eliminating rig The computational cost of such programs is O(n2). 4.2 Step (ii): abstraction application Step (ii) consists of the generation of an abstracted version of a given problem (an abstract context with new axioms and a new goal). This is performed by means of bridge rules, i.e. rules which allow us to derive facts in a context from one in another context: any application can be considered to be a form of inference in a multi-context system [Giu93]. In our example: 8 GMAP:: ABSTRACT ALPHABET BY kempe; `r' is declared to be a new indconst in `amap'. .... GMAP:: ABSTRACT ALLAXIOMS BY kempe; colours: n(y,b) and n(y,g) and n(y,r) and n(b,y) and n(b,g) and n(b,r) and n(g,y) and n(g,b) and n(g,r) and n(r,y) and n(r,b) and n(r,g); is a mapped axiom in `amap'. GMAP:: ABSTRACT GOAL exists r1 r2 r3 r4 r5 r6.( n(r1,r2) and n(r1,r3) and n(r1,r5) and n(r1,r6) and n(r2,r3) and n(r2,r4) and n(r2,r5) and n(r2,r6) and n(r3,r4) and n(r3,r6) and n(r5,r6)) BY kempe; exists r1 r2 r3 r6. (n(r1,r2) and n(r1,r3) and TRUE and n(r1,r6) and n(r2,r3) and TRUE and TRUE and n(r2,r6) and TRUE and n(r3,r6) and TRUE) is the mapped goal from `gmap'. 8 The lines which follow \;" and are before the prompt are ABSFOL's output. 7 The rst command completely generates the language of amap; the second abstracts all the ground axioms by adding the mapped axioms to amap; the last abstracts the goal. The whole action could have been achieved in only one step: GMAP:: ABSTRACT CONTEXT BY kempe; In such case the action becomes fully automatic. The simpli ed representation of the problem we have obtained is equivalent to the second pattern of Figure 1. 4.3 Step (iii): theorem proving in the abstract space By step (iii) we mean \standard" theorem proving in a (hopefully simpler) abstract context. Colouring a map is a typical form of backward theorem proving, from the goal to the axioms. Unfortunately, the implementation of backward inf |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://fandango.cs.unitn.it/~rseba/papers/wyoming.ps.gz |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
