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
|
{\rtf1\mac\deff2 {\fonttbl{\f0\fswiss Chicago;}{\f2\froman New York;}{\f3\fswiss Geneva;}{\f4\fmodern Monaco;}{\f6\fdecor London;}{\f8\fdecor San Francisco;}{\f11\fnil Cairo;}{\f12\fnil Los Angeles;}{\f13\fnil Zapf Dingbats;}{\f14\fnil Bookman;}
{\f16\fnil Palatino;}{\f18\fnil Zapf Chancery;}{\f20\froman Times;}{\f21\fswiss Helvetica;}{\f22\fmodern Courier;}{\f23\ftech Symbol;}{\f24\fnil Mobile;}{\f33\fnil Avant Garde;}{\f34\fnil New Century Schlbk;}{\f101\fnil Wartburg;}{\f118\fnil Warwick S;}
{\f128\fnil Moscow;}{\f129\fnil Russian;}{\f135\fnil MATH-BES;}{\f140\fnil Lovell;}{\f149\fnil Detroit;}{\f171\fnil XB Futura ExtraBold;}{\f176\fnil H Futura Heavy;}{\f201\fnil ¡Math;}{\f512\fnil Alexandrie;}{\f2500\fnil Konstanz;}}
{\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;}{\stylesheet{\f16 \sbasedon222\snext0 Normal;}}{\info{\title
Abstract for ICLP}{\author EBM}}\paperw11900\paperh16840\margl1080\margr1080\margt-1080\margb-720\widowctrl\ftnbj\fracwidth \sectd \sbknone\linemod0\linex0\cols1\endnhere \pard\plain \qc \f16 {\b\fs36 Permutations and computations\par
}\pard \qc {\b\fs20 \par
}\pard \qc 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 {\f23 f} from (sequent calculus) cut-free deriva
tions 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 con
jecture (but cannot yet prove) that {\f23 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 permutative 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 {\f23 \'da}L or {\f23 $}L), we show (i) that {\f23 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 {\f23 f} identifies two such derivations iff they are permutation-equivalent using just the permutations involving {\f23 \'c9}L, &L and {\f23 "}
L. Third, restricting even further to the language {\i D} of definite formulae and goals, we show (i) that {\f23 f }maps the simple uniform derivations of Miller [2] onto {\b EN} and (ii) (again, if the conjecture is true) that {\f23 f}
identifies two such derivations iff they are permutation-equivalent using just the permutations involving &L and {\f23 "}
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 integrat
ion 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]\tab Kleene,\~S.\~C.: Permutability of inferences in Gentzen\rquote s calculi LK and LJ, Mem. Amer. Math. Soc. (1952), 1\endash 26.\par
[2]\tab Miller,\~D.: A logical analysis of modules in logic programming, J. Logic Programming }{\b\fs22 6}{\fs22 (1989), 79\endash 108.\par
[3]\tab Miller,\~D.: Abstractions in logic programs, in: Odifreddi,\~P.\~(editor), Logic and computer science, vol. }{\b\fs22 31}{\fs22 of APIC Studies in Data Processing, Academic Press 1990, 329\endash 359.\par
}\pard \qj\fi-720\li720\sl240 {\fs22 [4]\tab Miller,\~D., G.\~Nadathur, F.\~Pfenning & A.\~Scedrov\~: Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic }{\b\fs22 51 }{\fs22 (1991), 125\endash 157.\par
}\pard \qj\fi-720\li720\sb40\sl240 {\fs22 [5]\tab Pfenning, F.: Unpublished lecture notes, 1994.\par
[6]\tab Prawitz,\~D.: Natural deduction, Almquist & Wiksell, Stockholm 1965.\par
}\pard \qj\fi-720\li720\sb40 {\fs22 [7]\tab Prawitz,\~D.: Ideas and results in proof theory, in:}{\fs26 }{\fs22 Fenstad,\~J.\~E.: Proc. of the second Scandinavian logic symposium, North-Holland 1971, 235\endash 308.\par
[8]\tab Zucker,\~J.: The correspondence between cut-elimination and normalization, Annals of Mathematical Logic}{\b\fs22 7}{\fs22 (1974), 1\endash 112.\par
}\pard \par
}
|
