This paper describes a new feature of the GAPT framework, namely the ability to import refutations obtained from external automated theorem provers. To cope with coarsegrained, under-speci ed and non-standard inference rules used by various theorem provers, the technique of proof replaying is employed. The refutations provided by external theorem provers are replayed using GAPT's built-in resolution prover (TAP), which generates refutations that use only three basic ne-grained inference rules (resolution, factoring and paramodulation) and are therefore more suitable for manipulation by the proof-theoretic algorithms implemented in GAPT.
Introduction
The use of coarse-grained, under-speci ed and non-standard inference rules is especially problematic for GAPT, because its proof transformation algorithms require that the proofs adhere to strict and minimalistic calculi, as is usually the case in proof theory. To solve this problem in a robust manner, the technique of proof replaying was implemented in GAPT.
In GAPT's historical predecessor CERES, a more direct translation of each of Prover9's inference rules into pre-de ned corresponding sequences of resolution and paramodulation steps had been implemented. Recomputing missing uni ers and guring out the obscure undocumented ways in which Prover9 assigns numbers to positions made this direct translation particularly hard. Thanks to the technique of proof replaying, these problems were avoided in GAPT.
The main purpose of this paper is to document how GAPT's internal resolution prover (TAP) was extended to support proof replaying and to report our overall experience with this technique. TAP outputs resolution proofs containing only ne-grained resolution, factoring and paramodulation steps, as desired.
Proof replaying is a widely used technique, and the literature on the topic is vast (see e.g. [Fuc97, Amj08, PB10, ZMSZ04, Mei00]). One thing that distinguishes the work presented here is that proofs are replayed into a logical system whose main purpose di ers substantially from the typical purposes (e.g. proving theorems, checking proofs) of most logical systems. GAPT's ongoing goal of automating the analysis and transformation of proofs can be seen as complementary and posterior to the goals of most other systems.
The rest of the paper is organized as follows: Section 2 describes the general algorithm for proof replay in our system and explains in more details how we implemented this algorithm for Prover9 output. In Section 3 we give a concrete example. The nal section concludes our work and discusses some future improvements. 2
Proof Replaying in GAPT The aim of this section is to describe how a proof from an external theorem prover is replayed in GAPT. At our disposal is the interactive prover TAP, which implements Robinson's resolution calculus [Rob65] and paramodulation. It is not e cient enough to prove complex theorems, but provided with an external proof it is often able to derive, for each inference step, the conclusion clause from its premises. In principle, if the conclusion clause C is not a tautology, a clause will be derived subsuming C by the forward computation of resolution (see [Lee67]). It works for any calculus with tautology-deletion. For our purposes, the specialized coarse-grained inference steps used in proofs output by optimized theorem provers have to be translated into a series of simple resolution and paramodulation steps. If this series is not too long, TAP will nd it and use it instead of the specialized inference rule used by the external prover. prover whose proof output can be parsed by GAPT can be used in place of Prover9, and we plan to add support for more external provers in the future. In the case of a successful result, the proof output is usually a text le, containing for each inference step its ID, a clause which was derived and a list of the rules which were applied4. The output le is then parsed into commands which steer TAP to replay the proof.
The API of TAP has two main modules: the search algorithm and the proof replay. The search space consists of elements called con gurations. Each con guration consists of a state, a stream of scheduled commands, additional arbitrary data and a result (possibly empty) which is a resolution proof. The state consists of the persistent data of the con guration and might be shared between di erent con gurations. A command transforms a con guration to a list of successor con gurations.
The so called \engine function" takes a con guration, executes the rst of its scheduled commands and inserts the newly generated con gurations into the search space. By default, the prover explores the search space using breadth- rst search, but this is con gurable.
We now describe the commands used for replay in more detail. In principle, we could replay an input proof purely using the Replay command. However, the actual implementation treats Prover9's inference rules assumption, copy and f actor specially because they do not create new proofs and are therefore translated directly into TAP commands. In the rst case, a proof of the assumption without premises is inserted into the list of derived clauses. In the second case, the guidance map containing the association of proofs to Prover9's inference identi ers is updated. Factoring is treated as a copy rule, because it is integrated into the resolution rule like in Robinson's original resolution calculus[Rob65]. Therefore we postpone the factoring of a clause until its next use in a resolution step. All other Prover9 inferences are replayed. The commands are grouped into di erent tasks: initialization, data manipulation and con guration manipulation. Guided commands are a subset of data commands. Table 1 provides an overview over the commands necessary for replay (commands in italics were speci cally added for replaying).
Initialization Commands Prover9Init
Replay Commands
Replay Con guration Commands SetStream PrependOnCond RefutationReached
Guided Commands AddGuidedInitialClause AddGuidedClauses GetGuidedClauses IsGuidedNotFound
Data Commands SetTargetClause SetClauseWithProof Variants Factor DeterministicAnd Resolve Paramodulation
InsertResolvent
The initialization commands interface TAP with an external prover. At the moment, there is only one command handling Prover9. It exports the given clause set to TPTP format, hands it over to Prover9, processes its output with the Prooftrans utility to annotate the inference 4Some provers have scripts translating their proof format to XML or TSTP. Since TSTP does not x the set of inference rules, some adjustments to the replaying have to be made for the di erent provers. In the actual system, a postprocessing to XML format is used which already separates the inference identi ers from the rule name and the list of clauses, but which does not apply any proof tranformations. identi ers, clauses and rule names with XML tags and uses Scala's XML library to parse the resulting proof into the system. Each assumption is registered together with its inference ID and put into the set of derived clauses (using AddGuidedInitialClause and InsertResolvent). The copy and the factor rules are treated by adding the proof with the new ID to the guidance map (using AddGuidedClauses). For all other rules, the replay command is issued.
The con guration commands allow control over the proof search process. It is possible to schedule insertion of additional commands into certain con gurations and to stop the prover when a (desired) resolution deduction is found.
All the data commands transform a con guration to a ( nite) list of successor con gurations. A simple example is SetTargetClause which con gures with which derived clause to stop the prover. Also the commands for the usual operations of variant generation, factoring, paramodulation and resolution are in this group. It also contains commands to insert a found proof into the set of already found derivations and a command for executing two commands after each other on the same state.
The purpose of the guided commands is the bookkeeping of derived proofs. It allows storage of the proof of a clause in a guidance map which is part of the state. When a guided inference is retrieved, the proof is put into the list of derived clauses within that state. There is also a special command looking for the result of a guided inference and inserting it into the set of derived clauses.
Replaying a rule rst needs to retrieve the proofs of the parent clauses from the guidance map. Then it creates a new TAP instance, which it initializes with these proofs as already derived clauses and the re exivity axiom for equality. The conclusion clause of the inference step to be replayed is set as target clause and the prover is con gured to use a strategy which tries alternating applications of the resolution and paramodulation rule on variants of the input clauses. Also forward and backward subsumption are applied after each inference step. In this local instance neither applications of the replay rule nor access to the guidance map is necessary. If the local TAP instance terminates with a resolution derivation, it is put into the global guidance map and returned as part of the con guration. In case TAP can not prove the inference, the list of successor states is empty. Since the scheduled replay commands are consecutive transformations on the same con guration, this also means the global TAP instance will stop without result. 3
An Example In this section we explain with a simple example how our algorithm works for a concrete proof. Consider the clause set from Figure 2, which was obtained from an analysis of a mathematical proof [BHL+06].
cnf( sequent0,axiom,'f'('+'(X1, X0)) = '0' | 'f'('+'(X0, X1)) = '1'). cnf( sequent1,axiom,~'f'('+'(X2, X1)) = '0' | ~'f'('+'('+'('+'(X2, X1), '1'), X0)) = '0'). cnf( sequent2,axiom,~'f'('+'(X2, X1)) = '1' | ~'f'('+'('+'('+'(X2, X1), '1'), X0)) = '1').
We give this clause set to Prover9, which outputs the refutation given on Figure 3. We see that the information contained in a rule description is incomplete { the uni er is normally left out and the variable names in the resulting clause are normalized. In many cases (such as in the last step) more than one step is applied at once. Clause 22 is rewritten twice into clause 3 (back rewrite(3),rewrite([22(2),22(8)])), yielding two equational tautologies (xx(a),xx(b)) which are deleted, resulting in the empty clause.
1 f(plus(A,B)) = zero | f(plus(B,A)) = one # label(sequent0) # label(axiom). [assumption]. 2 f(plus(A,B)) != zero | f(plus(plus(plus(A,B),one),C)) != zero # label(sequent1) # label(axiom). [assumption]. 3 f(plus(A,B)) != one | f(plus(plus(plus(A,B),one),C)) != one # label(sequent2) # label(axiom). [assumption]. 5 f(plus(A,B)) != zero | f(plus(C,plus(plus(A,B),one))) = one. [resolve(2,b,1,a)]. 11 f(plus(A,plus(plus(B,C),one))) = one | f(plus(C,B)) = one. [resolve(5,a,1,a)]. 16 f(plus(A,B)) = one | f(plus(C,D)) != one. [resolve(11,a,3,b)]. 20 f(plus(A,B)) = one | f(plus(C,D)) = one. [resolve(16,b,11,a)]. 22 f(plus(A,B)) = one. [factor(20,a,b)]. 24 $F. [back rewrite(3),rewrite([22(2),22(8)]),xx(a),xx(b)].
In our approach each (nontrivial) step is translated into a series of commands to the internal prover. The series of commands starts by initializing the prover with only those clauses contributing to the current inference and then schedules the resolution derivation. The last command of the series inserts the proof of the resolution step into the already replayed derivation tree.
In the example above, all steps except the last one are trivial steps and TAP returns exactly the same inferences. For the last step the following command is created:
List(ReplayCommand(List(0, 3, 22, 22), 24, ([], [])), InsertResolvent()) which says that from the re exivity predicate 0, clauses 3 and variants of 22 it should derive clause 24, i.e. the empty clause.
A full output of TAP for this example is too big to t nicely on a page.5 Since the only interesting case is the last step, Figure 4 displays the corresponding generated resolution derivation { in this case of the empty clause. 4
Conclusion In this paper we described GAPT's new feature of replaying refutations output by ATPs. Our approach is based on interpreting coarse-grained, under-speci ed and non-standard inference rules as streams of commands for GAPT's built-in prover TAP. By executing these commands, TAP generates resolution refutations containing only inference rules that are ne-grained and standard enough for GAPT's purposes. This approach is simpler to implement and more robust. The drawback is that its reliance on proof search by a non-optimized prover (TAP) makes replaying less e cient than a direct translation.
In the future, we plan to add support for the TSTP proof format, in order to bene t not only from Prover9 but from any prover using this format. As GAPT's algorithms for proof analysis and proof compression mature, we expect them to be of value in post-processing the proofs obtained by ATPs.
5The full output can be found here: http://code.google.com/p/gapt/wiki/PxTP2012 X , 1 _ X ( s u l p ( f ( = , ) e n o , ) ) 2 _ X , 3 _ X ( s u l p ( f ( = : ) 7 1 _ X > 0 _ X , 6 1 _ X > 1 _ X , 5 1 _ X > 2 _ X , 4 1 _ X > 3 _ X ( t n a i r a V ) 9 _ X > 1 _ X , 5 _ X > 2 _ X , 0 1 _ X > 0 _ X , 4 _ X > 3 _ X ( t n a i r a V : ) e n o , ) ) C , ) e n o , ) B , A ( s u l p ( s u l p ( s u l p ( f ( = , ) e n o , ) ) B , A ( s u l p ( f ( = ) e n o , ) ) 0 1 _ X , 9 _ X ( s u l p ( f ( = , ) e n o , ) ) 5 _ X , 4 _ X ( s u l p ( f ( = : ) e n o , ) ) 7 1 _ X , 6 1 _ X ( s u l p ( f ( = , ) e n o , ) ) 5 1 _ X , 4 1 _ X ( s u l p ( f ( = : ) 6 _ X > A , 8 _ X > C , 7 _ X > B ( t n a i r a V ) ) e n o , ) ) 5 _ X , 4 _ X ( s u l p ( f ( = ( r o t c a F ) ) e n o , ) ) 5 1 _ X , 4 1 _ X ( s u l p ( f ( = ( r o t c a F : ) e n o , ) ) 8 _ X , ) e n o , ) 7 _ X , 6 _ X ( s u l p ( s u l p ( s u l p ( f ( = , ) e n o , ) ) 7 _ X , 6 _ X ( s u l p ( f ( = ) e n o , ) ) 5 _ X , 4 _ X ( s u l p ( f ( = : ) e n o , ) ) 5 1 _ X , 4 1 _ X ( s u l p ( f ( = : = ) e n o , ) ) 7 _ X , 6 _ X ( s u l p ( f ( s e R ) e n o , ) ) 5 _ X , 4 _ X ( s u l p ( f ( = s e R : ) e n o , ) ) 8 _ X , ) e n o , ) 7 _ X , 6 _ X ( s u l p ( s u l p ( s u l p ( f ( = ) e n o , ) ) 5 1 _ X , 4 1 _ X ( s u l p ( f ( = s e R ) 3 1 _ X > 8 _ X , 2 1 _ X > 7 _ X , 1 1 _ X > 6 _ X ( t n a i r a V : ) e n o , ) ) 3 1 _ X , ) e n o , ) 2 1 _ X , 1 1 _ X ( s u l p ( s u l p ( s u l p ( f ( = ) e n o , ) ) 3 1 _ X , ) e n o , ) 2 1 _ X , 1 1 _ X ( s u l p ( s u l p ( s u l p ( f ( = s e R : [Amj08]
+ [BHL 06]