1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
{\rtf1\ansi \deff0\deflang1024{\fonttbl{\f0\froman Times New Roman;}{\f1\froman Symbol;}{\f2\fswiss Arial;}{\f3\froman Palatino;}}{\colortbl;\red0\green0\blue0;\red0\green0\blue255;\red0\green255\blue255;\red0\green255\blue0;
\red255\green0\blue255;\red255\green0\blue0;\red255\green255\blue0;\red255\green255\blue255;\red0\green0\blue127;\red0\green127\blue127;\red0\green127\blue0;\red127\green0\blue127;\red127\green0\blue0;\red127\green127\blue0;\red127\green127\blue127;
\red192\green192\blue192;}{\stylesheet{\f3\lang1036 \snext0 Normal;}}{\info{\title Abstract for ICLP}{\creatim\yr1994\mo7\dy1\hr15\min48}{\printim\yr1994\mo7\dy1\hr15\min50}{\version1}{\edmins0}{\nofpages1}{\nofwords484}{\nofchars3203}{\vern16433}}
\paperw11900\paperh16840\margl1080\margr1080\margt-1080\margb-720\gutter0 \widowctrl\ftnbj\hyphhotz425 \sectd \sbknone\pgnrestart\linex0\headery709\footery709\colsx709\endnhere \pard\plain \qc \f3\lang1036 {\b\fs36 Permutations and computations}{\b\fs36
\par }{\b\fs20
\par }Roy Dyckhoff
\par \pard \qc\sb240 School of Mathematical & Computational Sciences,
\par \pard \qc St Andrews University, St Andrews, Scotland
\par \pard \qc\sb240 rd@dcs.st-and.ac.uk
\par \pard \qj\sb240\sl320 {\b Abstract}. We consider the surjective Prawitz translation {\f1 f} from (sequent calculus) cut-free derivation
s to (natural) normal deductions, in order to examine the relationship between the uniform sequent calculus derivations of Miller, Nadathur, Pfenning & Scedrov [4] and the normal natural deductions of Prawitz [6,7] for first-order minimal logic. We conjec
ture (but cannot yet prove) that {\f1 f} identifies two such derivations iff they are permutation-equivalent, in the sense of Kleene\rquote s work [1] on permutations of intuitionistic derivations, a result similar to work of Zucker [8] on per
mutative conversions (for the system with cut and without the constants for disjunction and existential quantification). For the restricted language {\i fohH}
of first-order hereditary Harrop sequents (no occurrences of disjunctions or existential quantifiers that would trigger use of {\f1 /}L or {\f1 $}L), we show (i) that {\f1 f} maps the uniform derivations of [4] onto the set {\b EN}
of deductions in [6] expanded normal form; and (ii) (if the conjecture is true) that {\f1 f} identifies two such derivations iff they are permutation-equivalent using just the permutations involving {\f1 _}L, &L and {\f1 "}
L. Third, restricting even further to the language {\i D} of definite formulae and goals, we show (i) that {\f1 f }maps the simple uniform derivations of Miller [2] onto {\b EN} and (ii) (again, if the conjecture is true) that {\f1 f}
identifies two such derivations iff they are permutation-equivalent using just the permutations involving &L and {\f1 "}
L. This gives a bijection (also studied in [5]) from the set of uniform proofs with backchaining (a system [3] intermediate between sequent calculus and natural deduction) onto {\b EN}.
\par \pard \qj\fi360\sl320 Thus, the logic programmer\rquote s restriction to the use for {\i D}
of uniform proofs with backchaining is complete not merely (as is well-known) w.r.t. derivability but also, in a bijective fashion, w.r.t. the construction of expanded normal deductions. We anticipate these ideas to be useful in a proof-theoretic integra
tion of functional and logic programming (based on natural deduction and sequent calculus respectively).
\par \pard
\par \pard \qj\fi-720\li720\sb40\sl240 {\fs22 [1]}{\fs22 \tab }{\fs22 Kleene,}{\fs22 }{\fs22 S.}{\fs22 }{\fs22 C.: Permutability of inferences in Gentzen}{\fs22 \rquote }{\fs22 s }{\fs22 calculi LK and LJ, Mem. Amer. Math. Soc. (1952), 1}{\fs22 \endash }{
\fs22 26.}{\fs22
\par }{\fs22 [2]}{\fs22 \tab }{\fs22 Miller,}{\fs22 }{\fs22 D.: A logical analysis of modules in logic programming, J. Logic Programming }{\b\fs22 6}{\fs22 (1989), 79}{\fs22 \endash }{\fs22 108.}{\fs22
\par }{\fs22 [3]}{\fs22 \tab }{\fs22 Miller,}{\fs22 }{\fs22 D.: Abstractions in logic programs, in: Odifreddi,}{\fs22 }{\fs22 P.}{\fs22 }{\fs22 (editor), Logic and computer science, vol. }{\b\fs22 31}{\fs22
of APIC Studies in Data Processing, Academic Press 1990, 329}{\fs22 \endash }{\fs22 359.}{\fs22
\par }\pard \qj\fi-720\li720\sl240 {\fs22 [4]}{\fs22 \tab }{\fs22 Miller,}{\fs22 }{\fs22 D., G.}{\fs22 }{\fs22 Nadathur, F.}{\fs22 }{\fs22 Pfenning & A.}{\fs22 }{\fs22 Scedrov}{\fs22 }{\fs22
: Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic }{\b\fs22 51 }{\fs22 (1991), 125}{\fs22 \endash }{\fs22 157.}{\fs22
\par }\pard \qj\fi-720\li720\sb40\sl240 {\fs22 [5]}{\fs22 \tab }{\fs22 Pfenning, F.: Unpublished lecture notes, 1994.}{\fs22
\par }{\fs22 [6]}{\fs22 \tab }{\fs22 Prawitz,}{\fs22 }{\fs22 D.: Natural deduction, Almquist & Wiksell, Stockholm 1965.}{\fs22
\par }\pard \qj\fi-720\li720\sb40 {\fs22 [7]}{\fs22 \tab }{\fs22 Prawitz,}{\fs22 }{\fs22 D.: Ideas and results in proof theory, in:}{\fs26 }{\fs22 Fenstad,}{\fs22 }{\fs22 J.}{\fs22 }{\fs22
E.: Proc. of the second Scandinavian logic symposium, North-Holland 1971, 235}{\fs22 \endash }{\fs22 308.}{\fs22
\par }{\fs22 [8]}{\fs22 \tab }{\fs22 Zucker,}{\fs22 }{\fs22 J.: The correspondence between cut-elimination and normalization, Annal}{\fs22 s of Mathematical Logic}{\b\fs22 7}{\fs22 (1974), 1}{\fs22 \endash }{\fs22 112.}{\fs22
\par }\pard
\par
\par }
|
