We present a simple and e cient translation of the classical multi-succedent sequent calculus LK to natural deduction. This translation aims to produce few excluded middle inferences, and to keep the quanti er complexity of the instances of excluded middle low. We evaluate the translation on proofs imported from resolution-based rst-order theorem provers, and show that it achieves these goals in an e cient manner.
Program extraction realizes the computational content of mathematical proofs
as executable algorithms. These extractions, such as modi ed realizability [
Our particular interest lies in program extraction from classical proofs
using a method that interprets natural deduction proofs with excluded middle as
programs using exceptions [
GAPT [
Ultimately our goal is to extract programs from proofs generated by automated classical rst-order theorem provers. GAPT can already reliably import proofs in LK from more than half a dozen external theorem provers. In this paper we describe the missing piece to apply program extraction: a translation to natural deduction.
Translations of LK to natural deduction are as old as the proof systems
themselves. However these translations often focus on the preservation of provability,
and not on quantitative and qualitative aspects of the output. For example,
Gentzen rst presented such a translation using a Hilbert-style calculus as an
intermediate step [
Closer to our emphasis on the low amount of classical content is the recent
work of Gilbert [
Our translation uses a focusing approach and preserves the local shape of the
proof in a straightforward way. For example, a conjunction-right inference in LK
is typically translated to a single conjunction-introduction inference in natural
deduction. LK supports classical reasoning by allowing multiple formulas in the
succedent of a sequent, and inferences to operate on any one of these formulas.
We translate this switching between formulas in the succedent using a simulated
exchange rule that is similar in spirit to the constructor in -calculus [
We de ne the proof systems LK and natural deduction in Section 2. The translation from LK to natural deduction is then described in Section 3. Finally, Section 4 evaluates an implementation of the translation on real-world proofs generated by an automated theorem prover. 2
We consider rst-order formulas with standard connectives ^; _; ); :; >; ?, quanti ers 8; 9, and equality =. We denote formulas by A; B; C and D, variables by x and y, and constant terms by s, t and u. We write capture-avoiding substitution of x by y in A as A[y=x]. We present proofs as trees of inferences on sequents. A sequent A1; : : : ; An ` B1; : : : ; Bm is a pair of multisets of formulas interpreted as (Vin=1 Ai) ) Wjm=1 Bj . We denote multisets of formulas by ; ; and . We abbreviate union using comma: e.g., ; = [ and ; A = [ fAg. Negation of a multiset of formulas : is interpreted as f:A j A 2 g. The left-hand side of the sequent symbol is the antecedent, and the right-hand side is the succedent of a sequent. The sequent above the inference rule is the premise and the sequent below the rule is the conclusion. We will also write to refer to a proof with conclusion ` . `
Figure 1 lists the inference rules of the sequent calculus LK3. The inference rules of natural deduction (ND) are listed in sequent form in Figure 2. Our version of ND allows classical derivations by providing a rule for the excluded middle. We say the main formula of an inference rule in LK is the formula derived by the rule. For instance, for the (^:r)-rule the main formula is A ^ B. Induction rule for natural numbers: In the case of the natural numbers (constructors 0 of arity 0 and s of arity 1) the induction rules for LK and ND reduce to
Symmetry and transitivity of equality: Even though we only include re exivity and rewriting as inference rules for equality, symmetry and transitivity are derivable. The sequent calculus derivation of symmetry is depicted on the left and the natural deduction derivation on the right.
(re ) ` s = s (w:l) s = t ` s = s (= :r) s = t ` t = s s = t ` s = t s = t ` t = s (ax)
(= :i) ` s = s (= :e) The derivations of transitivity are as follows|again, sequent calculus on the left and natural deduction on the right.
s = t ` s = t (ax()w:l) ss == tt;;tt == uu `` ss == ut (= :r) s = t ` s = t (ax) ` s = s ((==::ie)) s = t ` t = s t = u ` t = u ((a=x:)e) s = t; t = u ` s = u Examples: We will illustrate the proof systems using a proof of double-negation elimination in sequent calculus on the left, and using natural deduction on the right.
A ` A (ax) ` A; :A (::r) ::A ` A (::l) ` ::A ) A ():r)
:A ` :A ((a:x:e)) ::::AA;; ::AA `` ?A ((e?m:e)) 3 Our implementation furthermore supports de nition and theory rules which we omit for brevity. Cut
` A; ` (w:l)
(^:l) A; B; ` A ^ B; ` A; ` B; ` A _ B; ; ` ; ` ; A :A; ` (::l) ` ; A B; ` A ) B; ; ` ;
(_:l) ():l) A[t=x]; ` 8xA; ` (8:l)
A[y=x]; ` 9xA; ` (9:l) ` ; A[y=x] ` ; 8xA (8:r) ` ; A[t=x] ` ; 9xA (9:r) The variable y must not occur free in , or A.
s = t; A[T=s]; ` s = t; A[T=t]; ` (=:l)
1 2 n S1 S2 : : : Sn 1; : : : ; n ` 1; : : : ; n; F [t] (ind) Each equation rule replaces an arbitrary number of occurrences of T .
A; A; ` A; ` (c:l) `` ; A (w:r) ` ; A; A (c:r) ` ; A ` ; A ` ; B (^:r) ; ` ; ; A ^ B ` ; A; B ` ; A _ B (_:r) A; ` ` ; :A (::r) A; ` ; B ` ; A ) B ():r) s = t; ` ; A[T=s] s = t; ` ; A[T=t] (=:r) ` > (>) ` t = t (re ) ? ` (?) The induction rule applies to arbitrary algebraic data types. Let c1; : : : ; cn be the constructors of a type and let ki be the arity of ci. Let F [x] be a formula def with x a free variable of the appropriate type. Then we call the sequent Si = F [x1]; : : : ; F [xki ]; i ` i; F [ci(x1; : : : ; xki )] the i-th induction step. `` ?A (?:e) ` 8xA ` A[t=x] (8:e) ` 9xA Quanti cation
; A ` C ; ; ` C The induction rule applies to arbitrary algebraic data types. Let c1; : : : ; cn be the constructors of a type and let ki be the arity of ci. Let F [x] be a formula def with x a free variable of the appropriate type. Then we call the sequent Si = F [x1]; : : : ; F [xki ]; i ` F [ci(x1; : : : ; xki )] the i-th induction step.
One of the main di erences between our sequent calculus and natural deduction is that natural deduction allows just a single formula in the succedent. In order to translate LK to ND our translation thus focuses on one formula in the succedent of the conclusion of the LK proof. The focused formula forms the succedent of the obtained ND proof, whereas the other formulas are negated and move to the antecedent. If possible, our algorithm directly proves the focused formula in ND. Otherwise, it rst exchanges the succedent formula of the ND proof with the needed main formula via the macro rule (ex) de ned in Figure 3, and then proves it. The translation then proceeds recursively up the LK proof tree. ; :A ` B (ex:A) ; :B ` A (a) Exchange macro rule.
A ` A (ax)
; :B ` A (b) De nition of the exchange rule.
:B ` :B
(ax) ; :B; :A ` ? (?:e) ; :B; :A ` A
(em) ; :A ` B (::e)
The translation function Tr takes two arguments. The rst argument is an LK proof with conclusion ` . The second argument is either an arbitrary formula in the succedent , say A, or if the succedent is empty and the argument is to be ignored. We call A the focused formula. Tr then produces an ND proof of the corresponding sequent, where the focused formula is the single formula in the succedent of the ND proof's conclusion:
If ` with A 2
, then and if
, then ` ` ? We de ne Tr inductively on the structure of the proof. We perform a case distinction on the last rule of the LK proof and on which formula is focused. Before presenting the case analysis, we revisit our example and demonstrate Tr by applying it to the proof of double-negation elimination in Figure 4. Inductive de nition of the translation Axioms: The axioms form the base cases:
Tr (
A ` A (ax) ; A) d=ef Tr ( ` t = t (re ) ; t = t) d=ef
A ` A (ax) ; ` t = t (=:i) ;
Tr ( Tr ( ` > ? ` (>) ; >) d=ef (?) ; ) d=ef ` > ? ` ? (>)
(ax)
Tr( ; A) ; :(
fAg) ` A Tr( ; ) : Tr Tr
(a) A ` A (ax) ` A; :A (::r) ; A ::A ` A ` ::A ) A ():i)
(c) A ` A (ax) ; A
A ` A
:A ` :A ((a:x:e)) :A; A ` ? (::i) :::AA``:AA (ex) ` ::A ) A ():i) (e) Tr
A ` A (ax) 1 ` A; :A (::r) ; AA
(::l) ::A ` A ::A ` A ` ::A ) A ():i)
(b) A ` A (ax) ` A; :A (::r) ; :A :::AA``:AA (ex) ` ::A ) A ():i)
(d) Exchange: For a right-inference rule ( :r) with 2 fc; _; ); :; 8; 9; =g, if the focused formula B is not the main formula A0, we rst derive A0 by changing the focus to A0 and add an exchange inference as follows:
Tr ` ; A; B 0 ` ; A0; B ( :r) ; B ` ; A; B 0 ` ; A0; B 0; : ; :B ` A0 0; : ; :A0 ` B ( :r) ; A0 (ex)
! ! def =
Tr We treat the binary rule (^:r) similarly. Let's consider the case where an arbitrary formula C, i.e., not the main formula A^B, coming from the right subproof r, is focused (symmetric if C comes from
Tr
l r ` ; A ` ; B; C (^:r) ; C ; ` ; ; A ^ B; C ! l): def =
l r 1 ` ; A ` ; B; C (^:r) ; A ^ BA ; ` ; ; A ^ B; C ; ; : ; : ; :C ` A ^ B ; ; : ; : ; :(A ^ B) ` C (ex) We want to point out that the use of (ex) is often not necessary, even if the succedent contains multiple formulas|namely when the main formula is already in focus.
We now present the derivations for left-inferences with arbitrary formulas in focus, and right-inferences with the main formula in focus4. Tr maintains the focused formula between recursive calls and does not unnecessarily change the focus. When we have to make a choice, we pick the rst formula in the succedent if it is non-empty, otherwise we set the focus to . There is a choice when translating (w:r) (when the weakening formula is in focus) and when translating (_:r). We omit cases where the succedent is empty and the focus is to be ignored if it does not a ect the structure of the translated proof.
Structural rules: The structural rules are translated as follows:
Tr Tr
Tr Tr
Tr
A; ` ; B (w:l) ; B
` ; B ` ; A; B (w:r) ; B ` ; A ` ; A; B (w:r) ; A ` ; A A; A; ` ; B (c:l) ; B A; ` ; B ` ; B; B (c:r) ; B ` ; B ! ! ! ! ! def = def = def = def = def =
Tr( ; B) ; : ` B A; ; : ` B (w)
Tr( ; A) ; : ` A :A; ; : `` BA ((ewx)) :B; ; :
Tr( ; A) ; : ` A :B; ; : ` A (w)
Tr( ; B) A; A; ; : ` B (c) A; ; : ` B B ` B (ax)
Tr( ; B) :B; ; : ` B (em) ; : ` B Cut: The cut rule is translated as follows. The focus should be on a formula from the right side of the cut. If the focus is instead on a formula D 2 from 4 The (w:r)-rule is a special case for which we also show the case where an arbitrary formula is in focus. the left side of the cut, we add an exchange inference (ex:D) after ():e).
Tr
l r ` ; A A; ` ; B (cut) ; B ; ` ; ; B !
Tr( r; B) d=ef Tr( l; A) A; ; : ` B ; : ` A ; : ` A ) B (())::ie)) ; ; : ; : ` B Propositional rules: Next, we present the translation of the propositional rules, starting with negation. If B is absent in the translation of the (::r)-rule (resulting in A; ; : ` ? being the conclusion of the translation of ) we can omit the (ax) and (::e) inferences.
Tr Tr
Tr
` A (::l) ; :A; ` :A; ` ; B (::l) ; B
` ; A; B ` ; :A; B (::r) ; :A A; ` ; B ! ! ! def = def = :A ` :A (ax)
:A; ` ?
Tr( ; B) :A; ; : ` B
The disjunction rules are handled next. If D is absent in the translation of the (_:l)-rule (resulting in B; ; : ` ? being the conclusion of the translation of r) we can omit the (ax) and (::e) inferences in the right branch of the derivation. The case where the focus is on D instead of C is symmetric. Tr
l r A; ` ; C B; ` ; D (_:l) ; C
A _ B; ; ` ; ; C; D ! def = :D ` :D ((a:x:e)) ` ; A _ B (_:r) ; A _ B ` ; A; B !
The implication rules are translated as follows. The translation of ():l) works similar to the translation of the cut rule: the focus should be on a formula from the right subproof. If the focus is on a formula D 2 instead, we add an exchange inference (ex:D) after the bottom-most ():e).
l r ` ; A B; ` ; C ():l) ; C A ) B; ; ` ; ; C ! def =
Tr( l; A) Tr Tr Tr Tr Tr Tr Tr
A[t=x]; ` ; B (8:l) ; B 8xA; ` ; B ` ; A[y=x] (8:r) ; 8xA ` ; 8xA A[y=x]; ` ; B (9:l) ; B 9xA; ` ; B ` ; A[t=x] (9:r) ; 9xA ` ; 9xA ! ! ! ! def = def = def = def =
Tr( ; B) A[t=x]; ; : ` B ; : ` A[t=x] ) B ():i)
8xA; ; : ` B Tr( ; A[y=x]) ; : ` A[y=x] ; : ` 8xA
(8:i) 9xA ` 9xA (ax)
Tr( ; B)
A[y=x]; ; : ` B 9xA; ; : ` B Tr( ; A[t=x]) ; : ` A[t=x] ; : ` 9xA (9:i) 8xA ` 8xA (ax) 8xA ` A[t=x] (8:e)
():e) (9:e) Equational rules: The equational rules are translated as follows: A ) B ` A ) B (ax)
; : ` A ():e) A ) B; ; : ` B
A ) B; ; ; : ; : ` C
Tr( r; C) B; ; : ` C ; : ` B ) C (())::ie)) ! def = Tr ` ; A ) B ():r) ; A ) B A; ` ; B ! def =
Tr( ; B) A; ; : ` B ; : ` A ) B ():i) Quanti er rules: The quanti er rules are handled as follows: s = t; A[T =s]; ` ; B (=:l) ; B s = t; A[T =t]; ` ; B
(ax) s = t ` s = t A[T =t] ` A[T =t] s = t ` t = s s = t; A[T =t] ` A[T =s] (ax)
(=:i) ` s = s (=:e) (=:e)
Tr( ; B) ss==t;t; A; :[T =s`]; A[;T:=s] `)BB ():i) s = t; s = t; A[T =t]; ; : ` B ():e)
s = t; A[T =t]; ; : ` B (c) Tr s = t; ` ; A[T =s] (=:r) ; A[T =t] s = t; ` ; A[T =t] ! Induction rule: The induction rule is translated as
Tr 1 2 n S1 S2 : : : Sn 1; : : : ; n ` 1; : : : ; n; F [t] (ind) ; F [t] ! def = Tr( 1; F1)
0 S1
Tr( 2; F2)
S20 : : : 1; : : : ; n; : 1; : : : ; : n ` F [t]
Tr( n; Fn)
Sn0 (ind) with
Si d=ef F [x1]; : : : F [xki ]; i; `
i; F [ci(x1; : : : ; xki )]; Si0 d=ef F [x1]; : : : F [xki ]; i; : i ` F [ci(x1; : : : ; xki )]; and
Fi d=ef F [ci(x1; : : : ; xki )]: Lemma 1. Tr terminates and is linear in the size of the LK proof. Proof. Tr either recurses and operates on a subproof with one less inference, or it recurses and changes the focused formula once and then operates on a smaller subproof. Hence Tr terminates. Each translation step is constant, hence Tr is linear in the size of the LK proof.
Optimizations: The translation of (_:r) seems inherently classical because the premise of the rule contains multiple formulas in the succedent. However, note that we can obtain an intuitionistic translation if the rule is preceded by a (w:r) inference, where the weakening adds one of the disjuncts. We make use of the following optimization, if the weakening immediately precedes the disjunction rule (symmetric if weakening with A instead of B):
Tr ` ; A ` ; A; B (w) ; A _ B ` ; A _ B (_:r) ! def =
Tr( ; A) ; : ` A ; : ` A _ B (_:i1)
Let us revisit the example in Figure 4: Notice that in the intermediate step in Figure 4d, the proof could be completed by inferring :A ` :A via (ax). The nave translation, as we presented it, instead continues and introduces an indirection into the ND proof. We make use of an optimization that catches such cases and stops the translation early by closing the proof with (ax): We check if the conclusion of the input proof is a sequent of the form ` A; :A with focus :A. If this is the case we simply return :A ` :A (ax) . The example proof when using the optimization is then translated as
:::AA``:AA ((eaxx)) ` ::A ) A ():i) which, after inlining the (ex) macro rule, is equivalent to the one presented in Section 2.
Translating constructive proofs: We want to point out that constructive LK
proofs are translated into constructive ND proofs|where constructive proofs
are proofs in intuitionistic logic. The constructive subset of LK that we
consider is essentially Gentzen's calculus LJ. The only di erence is the (_:r)-rule,
which in our calculus always has two auxiliary formulas in the succedent, and
hence requires special treatment. Other constructive subsets of LK, for example
multi-succedent calculi such as Maehara's L'J [
De nition 1. An LK proof is constructive if every sequent in the proof contains only a single formula in the succedent. The (_:r)-rule is an exception, which we consider to be constructive if it is immediately preceded by a weakening with one of the disjuncts.
De nition 2. An ND proof is constructive if it does not contain an (em) inference.
Lemma 2. Tr translates constructive sequent calculus proofs into constructive natural deduction proofs.
Proof. We analyze the cases which lead to introduction of an (ex) or (em) inference and show that they cannot occur: (i) The (c:r)-rule does not occur in a constructive proof. (ii) The (w:r) and (_:r) rules only occur together in constructive proofs and the optimization we described takes care of them. (iii) In ():l) and (cut), must be empty as we are dealing with single-succedent proofs, therefore the case where D 2 is the focus cannot occur. (iv) Finally, the focus never needs to be changed because we are dealing with single-succedent proofs. 4 4.1
Implementation and proof import
The translation described in Section 3 is implemented in our open source5 library
for proof transformations, GAPT [
The resulting proofs are imported in a multi-step process. Proof output from
the external provers is parsed and reconstructed using proof replay to obtain
resolution proofs. As the next step, we convert the resolution proofs to expansion
proofs [
We use expansion proofs as an intermediate step for two reasons: rst, they \clean up" the proofs considerably. Proofs produced by rst-order provers primarily record the proof search, and are not intended to be short, beautiful, or even constructive. Proof replay then adds additional complexity, in particular the reconstruction of a single equational inference in the prover output often produces several inferences in GAPT. All of this super uous complexity is completely ignored when passing to expansion proofs.
More importantly however, classical rst-order provers typically use
Skolemization as a preprocessing step. The freshly introduced Skolem functions are then
treated like any other function, and also equational inferences can rewrite the
arguments of the Skolem functions. In intuitionistic logic, Skolemization does not
always produce equivalid formulas: for example, the intuitionistic non-theorem
(:8x P (x)) ! 9x :P (x) is turned into the theorem (:P (c)) ! 9x :P (x) via
Skolemization. Given that we want to minimize the amount of non-constructive
reasoning, it is therefore of paramount importance to forgo Skolemization in this
sense. (It would of course also be possible to impose restrictions on the use of
Skolem terms so that they behave essentially like eigenvariables. However these
restrictions are typically not respected by the proofs produced by classical
rstorder provers. Hence either approach requires a transformation ensuring that
these restrictions are respected.) Expansion proofs allow us to straightforwardly
eliminate Skolem functions from rst-order proofs using a replacement
operation on the instance terms [
The expansion proofs are then converted to proofs in the sequent calculus LK
via a simple tableaux prover that reproduces the propositional parts of the proof
missing from the expansion proof. This proof import method described up to now
is not speci c to the translation to natural deduction described in this paper,
but is in parts independently used by many other applications implemented and
evaluated in GAPT, such as cut-introduction [
For our translation to natural deduction, we modify the conversion from expansion proofs to proofs in LK slightly using a simple heuristic: usually we want to apply the (::l)-rule as soon as possible (that is, close to the bottom) since it is an invertible unary inference rule that simpli es the sequent. However, it is not invertible intuitionistically|the premise may be unprovable even though the conclusion would be an intuitionistic theorem. We hence try the (::l)-rule last. 4.2
Large-scale tests
For the empirical evaluation of our translation, we took the 662 problems in the
rst-order FEQ, FNE, FNN, and FNQ divisions of the CASC-26 competition whose
size was less than one megabyte after including the separate axiom les. On these
662 problems, we used the translation on proofs imported from the E theorem
prover6 [
We set a total time limit of 5 minutes for each of these problems, and 2 minutes for the rst-order prover. Of the 662 problems, GAPT fails to clausify 15 of the problems due to excessive runtime. (These problems|e.g. HWV053+1|have blocks of more than a thousand quanti ers.) On the remaining 647 problems, E successfully returns 291 proofs. Using proof replay, GAPT reconstructs 285 resolution proofs, from there we get 283 expansion proofs, and then 261 proofs in LK. The translation to natural deduction nally results in 261 proofs. (These proofs do not contain induction inferences since E is a rst-order theorem prover.)
From a performance point of view, the runtime of the translation in Section 3 is negligible compared to the rest of the proof import. Figure 5 shows the relative runtime of the di erent proof import phases described in Section 4.1. The translation to natural deduction only makes up 0.65% of the total proof import time, making it practically feasible to obtain natural deduction proofs whenever necessary.
Parser CNF E replay ! exp. deskolem. ! LK ! ND 2.95% 3.58% 50.49% 12.50% 4.28% 7.89% 17.66% 0.65%
One of the main goals of the translation is to minimize the amount of nonconstructive reasoning in the produced proofs, that is, the number of the inferences for excluded middle as well as the complexity of their auxiliary formulas. Of the 261 natural deduction proofs produced, 154 (59%) do not contain any use of the excluded middle, and 224 (85%) do not contain quanti ed excluded middle, i.e., excluded middle on a formula that contains quanti ers. For applications in program extraction, excluded middle on quanti er-free formulas is 6 We picked the highest-ranking prover in the rst-order theorem category of the CASC-26 competition whose license allows competitive evaluation. typically not a problem since quanti er-free formulas are often decidable. Hence, it is important to consider the number of quanti ed excluded middle inferences. Figure 6 shows the average number of inferences for excluded middle grouped by the TPTP category of the problem. The problems in most categories require little use of the excluded middle (em), except for SYO, which contains syntactic problems that have no obvious semantic interpretation.
500 400 300 n a e m200 100 0 # excluded middle # quantified excluded middle 3 6 4 8 3 1 4 6
We can also interpret the quantitative results on excluded middle inferences
from the point of view of proof constructivization. If there are no uses of excluded
middle in the produced proof, then we have successfully converted an a priori
classical proof into an intuitionistic proof. Automated conversion of proofs
produced by classical rst-order theorem provers into intuitionistic logic has been
studied before using the Dedukti system and the Zenon prover: using a rewriting
system on natural deduction proofs [
A similar observation on the constructivity of classical proofs has been made
with the intuitionistic rst-order theorem prover ileanCoP [
Our proof deskolemization approach can fail if there are equational inferences that rewrite the arguments of a Skolem function. This only happens three times in the 283 expansion proofs considered here. The corresponding TPTP problems are GEO084+1, NUM855+2, and PRO004+1. It is not easy to pinpoint the failure to a single responsible inference in the proof output, since the input of the deskolemization algorithm is far away from the resolution proof and we only know that the deskolemized deep formula is not a tautology modulo equality.
In Section 3, we introduced a special case for (_:r) inferences that are directly following a (w:r) inference. Among the 802 (_:r) inferences in total, 349 (43.5%) directly follow a (w:r) inference, making this a worthwhile optimization. On average, the produced proofs in natural deduction contain 2.9 times as many inferences as the proofs in LK. 5
We have presented a simple translation of the sequent calculus LK to natural deduction. It is e cient and its cost is negligible compared to other processing steps. The produced proofs have few excluded middle inferences, and a large part of them are quanti er-free. A disadvantage of this translation is that it does not produce normal proofs in natural deduction. In particular the left-inferences in LK introduce redexes. We plan to address this issue by either normalizing the proofs in natural deduction, or simplifying the extracted programs.
As the next step we want to use the proofs generated by this translation in program extraction, and program synthesis using proofs generated by automated theorem provers.