\begin{center}
{\Large\bf CALL FOR PAPERS}
\vskip 0.4cm
{\Large\it Special Issue of the Journal of Automated Reasoning (JAR) on}
\vskip 0.3cm
{\Large\bf Computer Algebra and Automated Theorem Proving}
\vskip 0.5cm
{\it Editors: Deepak Kapur and Dongming Wang}
\end{center}
\vskip 0.9cm
Computer algebra (CA) methods are among some of the most powerful
ones developed for automated theorem proving (ATP) in several
specialized mathematical domains. Typical examples are algebraic
methods for ATP in geometry, which require complex and heavy
polynomial operations. ATP techniques are being incorporated into
the design and implementation of current CA systems. Research
projects have been exploring the cooperation, combination and
integration of CA and ATP systems.
This special issue is devoted to reporting significant research
developments and to motivating further investigations on the
interaction of CA and ATP (systems) in research, education and
industrial applications. Original research papers describing
recent advances and new insights on all aspects of coupling CA
and ATP are solicited. Specific topics of interest include (but
are not limited to):
\begin{itemize}
\item Incorporating ATP Mechanisms and Tools into CA Systems,
\item Combining CA and ATP Systems,
\item Applications of Combined Systems.
\end{itemize}
The deadline for submission is {\bf May 15, 1996}. All submitted
papers will be refereed according to the JAR refereeing
process. The special issue is expected to appear in 1997.
\vskip 0.3cm
Authors are invited to submit 3 copies of their manuscripts to
\bigskip\noindent
\begin{tabular}{lll}
Prof.\ Deepak Kapur & ~~~~~~~~or~~~~~~~~ & Dr.\ Dongming Wang \\
Department of Computer Science & & LIFIA--IMAG--CNRS \\
State University of New York & & 46, avenue F\'elix Viallet \\
Albany, NY 12222 & & 38031 Grenoble Cedex \\ \medskip
USA & & France \\
Fax: (1) 518 442 5638 & & Fax: (33) 76 57 46 02 \\
E-mail: kapur@cs.albany.edu & & E-mail: wang@lifia.imag.fr
\end{tabular}
\end{document}
%!PS-Adobe-2.0
%%Creator: dvipsk 5.55a Copyright 1986, 1994 Radical Eye Software
%%Title: cfp.dvi
%%Pages: 1
%%PageOrder: Ascend
%%BoundingBox: 0 0 596 842
%%EndComments
%DVIPSCommandLine: dvips -f cfp
%DVIPSParameters: dpi=300, compressed, comments removed
%DVIPSSource: TeX output 1995.11.24:1500
%%BeginProcSet: texc.pro
/TeXDict 250 dict def TeXDict begin /N{def}def /B{bind def}N /S{exch}N
/X{S N}B /TR{translate}N /isls false N /vsize 11 72 mul N /hsize 8.5 72
mul N /landplus90{false}def /@rigin{isls{[0 landplus90{1 -1}{-1 1}
ifelse 0 0 0]concat}if 72 Resolution div 72 VResolution div neg scale
isls{landplus90{VResolution 72 div vsize mul 0 exch}{Resolution -72 div
hsize mul 0}ifelse TR}if Resolution VResolution vsize -72 div 1 add mul
TR matrix currentmatrix dup dup 4 get round 4 exch put dup dup 5 get
round 5 exch put setmatrix}N /@landscape{/isls true N}B /@manualfeed{
statusdict /manualfeed true put}B /@copies{/#copies X}B /FMat[1 0 0 -1 0
0]N /FBB[0 0 0 0]N /nn 0 N /IE 0 N /ctr 0 N /df-tail{/nn 8 dict N nn
begin /FontType 3 N /FontMatrix fntrx N /FontBBox FBB N string /base X
array /BitMaps X /BuildChar{CharBuilder}N /Encoding IE N end dup{/foo
setfont}2 array copy cvx N load 0 nn put /ctr 0 N[}B /df{/sf 1 N /fntrx
FMat N df-tail}B /dfs{div /sf X /fntrx[sf 0 0 sf neg 0 0]N df-tail}B /E{
pop nn dup definefont setfont}B /ch-width{ch-data dup length 5 sub get}
B /ch-height{ch-data dup length 4 sub get}B /ch-xoff{128 ch-data dup
length 3 sub get sub}B /ch-yoff{ch-data dup length 2 sub get 127 sub}B
/ch-dx{ch-data dup length 1 sub get}B /ch-image{ch-data dup type
/stringtype ne{ctr get /ctr ctr 1 add N}if}B /id 0 N /rw 0 N /rc 0 N /gp
0 N /cp 0 N /G 0 N /sf 0 N /CharBuilder{save 3 1 roll S dup /base get 2
index get S /BitMaps get S get /ch-data X pop /ctr 0 N ch-dx 0 ch-xoff
ch-yoff ch-height sub ch-xoff ch-width add ch-yoff setcachedevice
ch-width ch-height true[1 0 0 -1 -.1 ch-xoff sub ch-yoff .1 add]/id
ch-image N /rw ch-width 7 add 8 idiv string N /rc 0 N /gp 0 N /cp 0 N{
rc 0 ne{rc 1 sub /rc X rw}{G}ifelse}imagemask restore}B /G{{id gp get
/gp gp 1 add N dup 18 mod S 18 idiv pl S get exec}loop}B /adv{cp add /cp
X}B /chg{rw cp id gp 4 index getinterval putinterval dup gp add /gp X
adv}B /nd{/cp 0 N rw exit}B /lsh{rw cp 2 copy get dup 0 eq{pop 1}{dup
255 eq{pop 254}{dup dup add 255 and S 1 and or}ifelse}ifelse put 1 adv}
B /rsh{rw cp 2 copy get dup 0 eq{pop 128}{dup 255 eq{pop 127}{dup 2 idiv
S 128 and or}ifelse}ifelse put 1 adv}B /clr{rw cp 2 index string
putinterval adv}B /set{rw cp fillstr 0 4 index getinterval putinterval
adv}B /fillstr 18 string 0 1 17{2 copy 255 put pop}for N /pl[{adv 1 chg}
{adv 1 chg nd}{1 add chg}{1 add chg nd}{adv lsh}{adv lsh nd}{adv rsh}{
adv rsh nd}{1 add adv}{/rc X nd}{1 add set}{1 add clr}{adv 2 chg}{adv 2
chg nd}{pop nd}]dup{bind pop}forall N /D{/cc X dup type /stringtype ne{]
}if nn /base get cc ctr put nn /BitMaps get S ctr S sf 1 ne{dup dup
length 1 sub dup 2 index S get sf div put}if put /ctr ctr 1 add N}B /I{
cc 1 add D}B /bop{userdict /bop-hook known{bop-hook}if /SI save N @rigin
0 0 moveto /V matrix currentmatrix dup 1 get dup mul exch 0 get dup mul
add .99 lt{/QV}{/RV}ifelse load def pop pop}N /eop{SI restore showpage
userdict /eop-hook known{eop-hook}if}N /@start{userdict /start-hook
known{start-hook}if pop /VResolution X /Resolution X 1000 div /DVImag X
/IE 256 array N 0 1 255{IE S 1 string dup 0 3 index put cvn put}for
65781.76 div /vsize X 65781.76 div /hsize X}N /p{show}N /RMat[1 0 0 -1 0
0]N /BDot 260 string N /rulex 0 N /ruley 0 N /v{/ruley X /rulex X V}B /V
{}B /RV statusdict begin /product where{pop product dup length 7 ge{0 7
getinterval dup(Display)eq exch 0 4 getinterval(NeXT)eq or}{pop false}
ifelse}{false}ifelse end{{gsave TR -.1 -.1 TR 1 1 scale rulex ruley
false RMat{BDot}imagemask grestore}}{{gsave TR -.1 -.1 TR rulex ruley
scale 1 1 false RMat{BDot}imagemask grestore}}ifelse B /QV{gsave
transform round exch round exch itransform moveto rulex 0 rlineto 0
ruley neg rlineto rulex neg 0 rlineto fill grestore}B /a{moveto}B /delta
0 N /tail{dup /delta X 0 rmoveto}B /M{S p delta add tail}B /b{S p tail}
B /c{-4 M}B /d{-3 M}B /e{-2 M}B /f{-1 M}B /g{0 M}B /h{1 M}B /i{2 M}B /j{
3 M}B /k{4 M}B /w{0 rmoveto}B /l{p -4 w}B /m{p -3 w}B /n{p -2 w}B /o{p
-1 w}B /q{p 1 w}B /r{p 2 w}B /s{p 3 w}B /t{p 4 w}B /x{0 S rmoveto}B /y{
3 2 roll p a}B /bos{/SS save N}B /eos{SS restore}B end
%%EndProcSet
TeXDict begin 39158280 55380996 1000 300 300 (cfp.dvi)
@start /Fa 8 122 df<12FEA7123CA21278127012F0070C7C860F>44
D<137013F81203127F12FFA312431203B3A6387FFF80B512C0A26C138012247CA31B>49
D<381FFFE04813F0A314E0EB8000A713FEEBFF8014C014E0EB87F01303123E001C13F812
00A61220A2007013F0EA7807EAFE0F387FFFE06C13C06C13806C1300EA03F815247EA21B
>53 D<EB3F803801FFC05A5A380FE040381FC000485A90C7FC5AA2127EA238FE3F80EB7F
C0EBFFE0B512F0EB83F8130114FC12FEA7127EA3007F13F8EA3F031387381FFFF06C13E0
6C13C06C13803800FE0016257EA31B>I<EA01FCEA07FF4813C04813E0EA3F87387F03F0
127EEB01F812FEA214FCA8EA7E03127F1307EA3FFFEA1FFDEA0FF9EA07F1380001F8A213
03A214F0EA0807380C1FE0381FFFC014804813006C5AEA07F016257EA31B>57
D<007FEC01FE486CEB03FFA36D5BA2D8FDE0EB0FBFA26D131F00FC153FA26D133F017813
3E017C137EA2013C137C013E13FCA290381F01F8A2010F13F01483A2903807C7E0A29038
03EFC0A3903801FF80A26D1300A3147E007890C7121E28237CA231>77
D<48B4FC000F13C04813E014F0381E07F8EA180312101200A2137FEA07FFEA1FE3EA3F83
EA7F0312FEA31307EA7F0F13FB123FEA1FE33807C1F015177F961A>97
D<007C137800FE13FC007E13F8EA7F01123F14F0EA1F83A2EBC3E0EA0FC7A2EA07E714C0
120313EF1480EA01FFA26C1300A27F137EA3137CA213FC5B1261EA7FF05B5B90C7FC1621
7F9619>121 D E /Fb 1 16 df<EA03F0EA0FFC487E487E481380A2B512C0A86C1380A2
6C13006C5A6C5AEA03F012147D9519>15 D E /Fc 67 124 df<1478137C13FC12013803
C0005B1207A838FFFC78A3EA0780B3152480A31A>12 D<EA03C0EA0780EA0F00120E121E
5A5A12705A0A0977A218>19 D<137013E0EA01C01203EA078013005A120E121E121C123C
A212381278A4127012F0AE12701278A41238123CA2121C121E120E120F7E1380EA03C012
01EA00E013700C327DA413>40 D<12E012707E123C7E120E120F7E1380120313C0A21201
13E0A4120013F0AE13E01201A413C01203A21380120713005A120E121E5A12385A5A0C32
7DA413>I<1278A412181230A21260A212E0050A7C830E>44 D<EAFFF8A30D03808C10>I<
12F0A404047B830E>I<EA01F0EA07FC487EEA1F1F383C0780A2387803C0A3EA700100F0
13E0AF387803C0A4383C0780A2381F1F00EA0FFE6C5AEA01F013237EA118>48
D<1340EA01C0120712FFA212FB1203B3A7B5FCA310227CA118>I<EA03F0EA0FFC487EEA
3C1F38300780387003C0126000E013E0EAC0011240A21200A3EB03C0A2EB0780A2EB0F00
131E5B5B5B485A5B485A48C7FC120E5A5A5AB512E0A313227EA118>I<EA03F0EA07FCEA
1FFFEA3E0F38380780387003C01220A21200A3EB0780A2EB0F00133EEA03FC5B13FEEA00
0FEB0780EB03C0A2EB01E0A5128038C003C012E038700780EA3C0F381FFF00EA0FFCEA03
F013237EA118>I<131FA2132FA2136F13EF13CF1201A2EA038FA21207130F120F120E12
1E123CA21278A212F0B512F8A338000F00A915217FA018>I<387FFF80A30078C7FCA9EA
79F8EA7BFCEA7FFFEB0F80EA7E07387C03C01278380001E0A7384003C0A212E038700780
387C1F00EA3FFEEA0FFCEA03F013227EA018>I<137E48B4FC5AEA07C148C7FC121EA25A
A25AA213F8EAF1FEEAF7FF38FF0F80EAFC0738F803C0A2130100F013E0A51270A21278EB
03C01238003C1380EA1C07381F0F00EA0FFE6C5AEA01F013237EA118>I<B512E0A3C7FC
EB01C0EB038013071400130E131E131C133C13381378A25BA25B1201A3485AA5485AA713
217EA018>I<EA01F0EA07FC487EEA1E0F383C0780A2387803C0A500381380EA3C07381E
0F00EA0F1EEA07FC6C5AEA0FFEEA1E0F383C0780387803C0A238F001E0A6387803C0A238
3C0780EA3E0F381FFF00EA07FCEA01F013237EA118>I<EA01F0EA07FC487EEA1E0F487E
00381380EA780314C012F0130114E0A6EA70031278A2EA3C07EA3E1FEA1FFDEA0FF13803
E3C0EA0003A21480130714005BEA201EEA383CEA7FF86C5AEA0FC013237EA118>I<12F0
A41200AE12F0A404167B950E>I<EB0FE0EB7FF8497E3803F03E3807C01F48487E903803
FF80EA1E07485AEB1E1F39783C0FC0EB7807A212F0EBF003A790387807801278A290383C
0F00383C1E1EEB0FFC6C6C5A6C6C5A0180C7FC3907C003C03903F00F80C6B51200EB7FFC
EB0FE01A237DA221>64 D<EB0F80A2497EA2131DEB3DE013391338EB78F0A2EB7070EBF0
78A213E000017FA213C000037FA2138000077FA290B5FC481480A2380E0007001EEB03C0
A24814E01401A24814F01400A24814F81D237FA220>I<EB0FF0EB7FFC90B5FC3801F01F
3807C00749C7FC48C8FC121E123E123CA25AA35AA91278A37EA2123E121E7E6C6C1380EB
C0033801F00F6CB51200EB7FFCEB0FF019257DA31F>67 D<EAFFFEEBFFC08038F003F0EB
00F8147C80141E80A2EC0780A3EC03C0A915801407A3EC0F005C141E5C14F81303B512E0
5C49C7FC1A237BA223>I<B512F0A300F0C7FCACB512E0A300F0C7FCAEB512F8A315237B
A21D>I<B512F0A300F0C7FCADB512C0A300F0C7FCB014237BA21C>I<EB0FF0EB3FFE90B5
12803801F80F3803E003D80780C7FC48C8FC121EA25AA25AA35AA6ECFFC0A300781303A3
7EA27EA27EEA0780EA03E03801F8076CB5FC013F1300EB0FF81A257DA321>I<12F0B3B1
04237CA20D>73 D<130FB3ADEAC01EEAF03EEAFFFCEA7FF8EA0FE010247EA217>I<00F0
EB0F80EC1F00143E5C5C495A495A5C1307495A49C7FC133E5B5B12F1EAF3FCA2EAF7DEEA
FF9F130F486C7E00FC7FEAF803486C7EA26D7E80147880143E141E80A2EC078015C01A23
7BA222>I<12F0B3AEB512C0A312237BA21A>I<00FC147E6C14FEA300F7EB01DEA3EB8003
00F3149EA2EBC007A200F1141EA2EBE00F00F0130EA2EBF01EA2EB701CEB783CA2EB3838
EB3C78A2EB1C70A2EB1EF0EB0EE0A2130FEB07C0A390C7FC1F237BA22A>I<00FC131E7E
A312F7A2EAF380A213C012F1A213E012F013F0A21378A21338133CA2131EA2130E130F13
07A2149E1303A2EB01DEA2EB00FEA3147E17237BA222>I<EB1FC0EB7FF03801FFFC3803
F07E3807C01F390F800F80391F0007C0001E130348EB01E0A248EB00F0A30070147000F0
1478A9007814F0A3007C1301003C14E0003E1303001E14C0001F1307390F800F803907C0
1F003803F07E6CB45A38007FF0EB1FC01D257DA324>I<EAFFFEEBFF8014C038F003E0EB
00F01478A2143CA61478A214F0EB03E0B512C01480EBFE0000F0C7FCAF16237BA21F>I<
EAFFFCEBFF8014C038F003E0EB00F014781438143CA51438147814F0EB03E0B512C01480
EBFE00EAF01E7FA2EB0780130314C0EB01E0A2EB00F0A21478A2143C141EA2140F18237B
A21F>82 D<13FF000313C04813F0EA1F81381E0070481300A25AA5127C123C123FEA1FC0
EA0FFC6CB4FC0001138038003FC0EB07E0EB01F0130014F81478A600C013F07E38F801E0
387E07C0383FFF80000F1300EA01FC15257EA31B>I<B612F0A3D8000FC7FCB3AE1C237E
A221>I<00F0133CB3A900781378A36C13F0381E01E0EA1F87380FFFC000031300EA00FC
16247BA221>I<00F01478A2007814F0A36CEB01E0A36CEB03C0A36CEB0780A213800007
EB0F00A23803C00E141EA23801E01C143CA23800F0381478A2EB787014F0A2EB38E0133D
EB1DC0131FA26D5AA21D237FA220>I<00F0011FEB01E0EC3F80A2007816C0027B130315
C014736C0171EB078014F115E014E16C01E0EB0F00130115F014C0000FEC701E13031578
1480D80783EB381C163C0187133C000301001338151C01C7147813CFD801CEEB1E70150E
A201EE14F0D800EC5C01FC1307A301785C2B237FA22E>I<00F8143E007C147C003C1478
003E14F86C14F06CEB01E0EB8003D807C013C00003130701E013803901F00F0000005BEB
F81EEB783EEB3C3CEB3E78131E6D5A5C13076D5AAF1F2380A220>89
D<EA07F0EA3FFC487EEA781FEA400F38000780A4137FEA07FF121FEA3E07127812F0A313
0FEA7C1FEA7FFFEA3FF7EA1F8711167E9517>97 D<12F0AD13F8EAF3FEB5FC38FE0F80EA
F80738F003C0A2EB01E0A7130314C0A238F80780EAFE1F38F7FF00EAF3FCEAF1F813237D
A219>I<EA01FCEA07FF481380EA1F03EA3C0148C7FCA2127012F0A61278A36C1340381F
03C0EA0FFF6C13803801FC0012167E9516>I<EB01E0ADEA03E1EA0FF9EA1FFFEA3F07EA
3C03EA7801A212F0A812781303123CEA3E0FEA1FFDEA0FF9EA03E113237EA219>I<EA01
F8EA07FE487E381F0780383C03C0EA7801A2387000E0B5FCA300F0C7FCA312701278127C
6C1340381F03C0EA0FFF6C13803800FC0013167F9516>I<137FEA01FF5AEA07C013005A
A8EAFFF8A3EA0F00B3102380A20F>I<3803F078380FFFF85A383E1F00EA3C0F38780780
A5383C0F00EA3E1FEA1FFE485AEA33F00070C7FCA21278EA3FFEEBFFC06C13E04813F0EA
780138F000F81478A4007813F0383E03E0381FFFC06C13803801FC0015217F9518>I<12
F0ADEAF1F8EAF3FCEAF7FEEAFE1EEAF80FA212F0B010237CA219>I<12F0A41200A912F0
B3A404237DA20B>I<13F0A41300A913F0B3A91280EAE3E012FFEA7FC0EA1F000C2D83A2
0D>I<12F0ADEB1F80EB3F00133E5B5BEAF1F0EAF3E0EAF7C012FFA27FA2EAFDF0EAF8F8
EAF078137C7F131E131F7F1480EB07C012237CA218>I<12F0B3B104237DA20B>I<39F0F8
07C039F3FE1FF039F7FF3FF839FE0F707800FCEBE07C39F807C03CA200F01380AF1E167C
9527>I<EAF1F8EAF3FCEAF7FEEAFE1EEAF80FA212F0B010167C9519>I<EA01FCEA07FF48
1380381F07C0383C01E0387800F0A20070137000F01378A6007813F0A2EA7C01383E03E0
381F07C0380FFF806C1300EA01FC15167F9518>I<EAF0F8EAF3FEB5FC38FE1F80EAF807
38F003C0A214E01301A6130314C0130700F81380EAFE1F38F7FF00EAF3FCEAF1F800F0C7
FCAA13207D9519>I<3803E1E0EA07F9EA1FFD130FEA3C03127CEA780112F812F0A612F8
12781303123CEA3F0FEA1FFDEA0FF9EA03E1EA0001AA13207E9519>I<EAF0E012F312F7
EAFF005A5A5AA25AAE0B167C9511>I<EA07F0EA1FFCEA3FFEEA3C0EEA78061300A2127C
123F13F0EA1FF8EA0FFCEA01FEEA001F130FA312C0EAF81EEAFFFEEA3FFCEA0FF010167F
9513>I<121EA6EAFFFCA3EA1E00AE1308EA1F1CEA0FFC13F8EA07C00E1C7F9B12>I<EAF0
0FB1131FEAF83FEA7FFF13CFEA1F0F10167C9519>I<38F001E0A212F8387803C0A2003C
13801307A2001E13005BA2EA0E0EEA0F1EA2EA071C139C13BCEA03B8A213F86C5AA21316
7F9516>I<39F007803CEB0FC0A2D8780D1378131D14E0131CD83C1813F0133814F0001C
14E0001E137113701479000EEB39C01360000F133B00071480141BEBC01FA2000314001E
167F9521>I<007813F0387C01E0383E03C0EA1E07000F138038078F0013DEEA03FE6C5A
6C5A137013F8487EEA03DC139EEA078F380F0780121EEB03C0383C01E0387800F000F813
F81516809516>I<38F001E0A2387803C0A2127C383C0780A2121EEB0F00A2120F130E13
1E1207139C1203139813B8120113F01200A25BA212015BA2485A1207007FC7FCA2127C13
207F9516>I<387FFFC0A338000F801400131E133E5B13785B1201485A5B485A120F48C7
FC121E5A127CB512C0A312167F9515>I<B512FEA31703808E18>I
E /Fd 19 118 df<EA0780EA0F00A3C7FCAE1278A25AA209167B950E>58
D<3801FFFEECFF8015C09038E007E03903C001F014001578A2153C485AA548C7FCA41538
001E1478A315F05AEC01E0A2EC03C0EC078048EB0F00141E147C495A387FFFF0B512C091
C7FC1E237BA223>68 D<48B512E0A301E0C7FC485AA5485AA548C8FCEBFFFEA390C8FC12
1EA45AA55AA4387FFFFCB55AA21B237BA21D>I<D801E0131F153E157C15F83903C001F0
EC03C0EC0F80EC1F00143E48485A5CEB81F0EB83E0EB87C0EA0F0F131F133FEBFBE013F1
381FE1F013C01380EB0078123E003C137C143C143E141E5A141F80158014075A15C02023
7BA222>75 D<00F0D91F8013F0023FEB01E0A2027FEB03C0147702F7EB078014E7EE0F00
EA780102C3131E130302835B130702031338010F1478010E1470011E14F0011C5C013C13
811338ED83C013780170EB878001F013C701E091C7FC00795C01C0138E159ED87B80139C
123B010013B8003F14F8003E5C1401003C5C2C2378A22E>87 D<13FE3803FF80000F13C0
EB03E0EA08011200A4131F3803FFC0120FEA1F03123C127838F00780A2130FEAF83FEA7F
FFEBEF00EA3F8F13167D9517>97 D<140FA4141EA5143CA413FC3801FF78000713F8EA0F
C1EA1F00121E4813F0A25AA238F001E0A5EB03C0A2EA780FEA7C1FEA3FFB381FE780EA0F
8718237CA219>100 D<133F3801FFC05A3807C3E0EA0F00001E13F04813701238387FFF
F0A2B512E000F0C7FCA51278007C1380EA3E07EA3FFF380FFE00EA03F014167D9516>I<
90380F83C0EB3FEF90B5FC3901F0F8003803C078A2EA0780A35CA23803C3E0EBFFC0485B
D80E7CC7FC000CC8FC121C121E381FFF806C13E080487FEA3C00481378A25AA25CEAF801
387E07E06CB45A6C90C7FCEA03F81A21809518>103 D<EA01E0A2EA03C0A2C7FCA9EA07
80EA0F00A5121EA45AA55AA55AA20B237DA20B>105 D<EA01E0A4485AA5485AA414F838
0F01F0EB03E0EB07C0EB1F80EB3F00EA1E7E5BEA1FF07F123F7F137CEA3E3E123CEA781E
131FA2EB0F80A2EAF00714C015237CA218>107 D<39078FC07E390F3FE1FFD97FF31380
9038E0F707EB80FCEB00F85A001E13F0A33A3C01E00F00A5397803C01EA54848485AA221
167C9527>109 D<38078F80380F3FC0EB7FE013E113811301121F121EA3383C03C0A538
780780A538F00F00A213167C9519>I<133FEBFFC0000313E03807C1F0380F00F8001E13
785A143C5AA2481378A314F814F0EB01E01278387C07C0383E0F80383FFF00EA0FFCEA07
F016167D9518>I<3801E3F03803CFF8EBDFFCEBF87EEBE01E13C03807801F140FA3380F
001EA4143C001E137C001F1378EB01F0EB83E0EBFFC0003C1380EB3E0090C7FCA25AA55A
A318207F9519>I<EA078FEA0F1E137E13F013C01380EA1F00A2121EA25AA55AA55AA210
167C9511>114 D<137E3801FF80000713C01381380F00801400121E121F7FEA0FF8EA07
FE6C7EC6FC130F14801400A212C0EAF03EEAFFFC6C5AEA0FE012167E9513>I<EA0780A2
EA0F00A4EA7FFEEAFFFCA2EA1E00A35AA45AA55AA21340EAF1C012FFEA7F80EA7E000F1C
7B9B12>I<000F13F0381E01E0A5383C03C0A438780780A538F00F00A25B137FEAFFEFEA
7FDEEA3F1E14167B9519>I E /Fe 24 118 df<EC0780EC0F00141E5C5C14F8495A495A
5C495A130F91C7FC5B133E133C137C137813F85B1201A2485AA25B1207A2485AA348C8FC
A4123EA55AA5127812F8AF1278A2127CA3123C123E121EA2121F7E6C7EA26C7E194979B5
1A>40 D<EB01E06D7E1478A280A280A2141FA280A21580A41407A415C0A21580A3140FA7
EC1F00A6143EA45CA35CA3495AA3495AA2495AA25C130F91C7FC5B133EA25B13785B1201
5B485A485A48C8FC121E5A5A5A1A4980B51A>I<ED1FC0A2153FA2157F157715F7A29138
01E7E0140315C714071587EC0F831503021F13F0141E143E147CA214F814F013019138E0
01F8130314C01307EB0F80A2EB1F0016FC49B5FCA25BA201F8C7FC485AA2484814FE167E
485AA2485A48C8FCA2003E157FA248153FA25A28327EB12D>65 D<EB1F80EB3F00A4137E
A55BA5485AA4485AA5485AA5485AA5485AA448C7FCA5127EA55AA211327AB113>73
D<ED1F80ED3F00A4157EA55DA54A5AA44A5AA54A5AA54A5AA54A5AA44AC7FCA4147E0060
13FE387001FCEAF803B55A5C6C13C0001F5BD803FCC8FC21337CB120>I<90381FFFFE49
EBFFC016E016F891380007FC017E1301ED00FE167E163FA25BA54848147EA216FCA24848
EB01F8ED07F0ED0FE0ED7FC090B61200485C15F015C09038E007E0A2EA0FC06E7EA36E7E
EA1F80A26E7EA248C7FC157EA381127EA2ED1F80A348EC0FC0A228327AB12B>82
D<EC07F8EC3FFF91B512C04914E04914F0903907F80FE090380FE00390381F800149C712
C01640017E1400A25BA67FA27FEB7FE014FC6DB47E6D13E06D7F01037FEB007FEC0FFC14
016E7EA2157EA75DA20020495A12300078495A007C495AB4130F9038E03FC06CB55A6C49
C7FC000F5B000313F038007FC024347CB225>I<EB0FF0EB7FFC48487E487F9038E01F80
3807800FEA0600000414C0C71207A2EC0F80A3EB01FF133F48B512001207381FF01FEA3F
80387E003E127C5AA2147E147CEB01FCEAFE07B5FC6C137CEBFCF8EA1FC01A1F7B9E20>
97 D<EB03FE90381FFF804913E090B512F03901FC03E03803F000D807C0136048481300
48C8FCA2123EA25AA35AA77E007C1303007E13066C131EEB80FEEA1FFF6C13F8000313E0
C690C7FC1C1F7B9E1E>99 D<ED07C0ED0F80A4ED1F00A5153EA55DA4903807E0F8EB1FFC
EB7FFE90B5FC3801FE0F3903F003F0EA07E0380F8001121F1300003E495AA25AA348495A
A44A5AA46C131F007C49C7FC007E5B383F81FFEBFFDF6C139F3807FE3EEA01F822327BB1
23>I<EB03F0EB1FFCEB7FFF90B5FC3901F81F803803F00F3907C007C0EA0F80381F0003
121E123E003FB5FC5AA300F8C8FCA8127C007E13026C130EEB80FEEA1FFF6C13F86C13E0
C690C7FC1A1F7B9E1E>I<EC3FE0ECFFC013035B90380FC08049C7FC133E133C137CA25B
A5485AA4B512C0A4D803E0C7FC485AA5485AA548C8FCA4123EA55AA55AA21B3279B115>
I<027E13F8903801FF8F010713FF5B90391F83F80090383E01F0137CA2EBF8001401EA01
F0A34A5AA24A5A3800F80F6D485A90B5C7FC485B38039FF8EB87E0D80780C8FCA4EBFFFC
ECFF806C14E04880121F393F0007F8003E13014813005AA34A5AA26C495A007EEB0FC039
7F807F806CB5C7FC6C5B000713F0C61380252E7F9E22>I<131F133EA45BA55BA5485AA4
3803E07E9038E3FF8001E713C013EF9038FE0FE03807F807EBF00313E0A213C0000FEB07
C01380A4391F000F80A4003EEB1F00A548133EA5485BA21B327AB123>I<137EA313FCA3
1300ABEA03E0A5EA07C0A5EA0F80A5EA1F00A4123EA55AA55AA20F307BAF10>I<131F13
3EA4137CA513F8A5EA01F0A4EA03E0A5EA07C0A5EA0F80A5EA1F00A4123EA55AA55AA210
327BB110>108 D<2603E07FEB1FC0903AE1FFC07FF001E79038E1FFF801EF13E3903AFE
07F781FC3A07F803FE00496C48137C01E05BA201C05B000F010314F801805BA43B1F0007
C001F0A4003E90390F8003E0A54890391F0007C0A548013EEB0F80A22E1F7A9E36>I<38
03E07E9038E3FF8001E713C013EF9038FE0FE03807F807EBF00313E0A213C0000FEB07C0
1380A4391F000F80A4003EEB1F00A548133EA5485BA21B1F7A9E23>I<EB03FCEB0FFF01
3F138090B512C03901FC0FE03903F003F03807C001390F8000F848C7FC1578003E147CA2
5AA215784814F8A3EC01F0A2EC03E0A26CEB07C0007C130F007EEB1F806CEB3F00EBC1FE
381FFFF86C5B000313C0C648C7FC1E1F7B9E22>I<90387C0FC0EC7FF090387DFFF8017F
7FECC1FE9038FF007F01FC7F5B811680485A150FA3ED1F00485AA3153E485A157E157C5D
1401000F495A9038E00FE09038F03FC090B55AD9BFFEC7FC381F1FFCEB07E090C9FCA212
3EA55AA55AA2212D7D9E23>I<3803E03C14FC13E313E713EF3807DFC0EBFE005B13F05B
120F5B5BA348C7FCA4123EA55AA55AA2161F7B9E17>114 D<EB0FF8EB7FFF90B512C05A
3903F00F803807C0034848C7FCA57F13FC3807FFC06C13F06C7F6C6C7E130FEB00FE147E
143EA300405B126000785BEAFE03B55A6C5B001F1380D803FCC7FC1A1F7D9E1A>I<EA01
F0A5485AA4B512E0A43807C000485AA548C7FCA5123EA45AA512FC1304131CEAFFFC127F
5BEA3F80132879A718>I<3907C003E0A5390F8007C0A5391F000F80A5003EEB1F00A448
133EA4147E485BEAFC011307B5127CEA7FFE383FF8F8EA1FC01B1F799E23>I
E /Ff 26 119 df<EC7FF84A7E497FA3497FA3498014FDA2D90FF97FA214F8011F805CA2
013F6D7E14E0A2017F6D7EA214C001FF6D7EA21480486E7EA21400486E7EA248481580A2
90B7FC4816C0A34816E0A201F8C7FC484815F0167FA2484815F8163FA2484815FC161F5B
6CC8EA0FF82E327DB135>65 D<EC1FFF49B512E0010714FC011F14FF137F90B7FC5A4890
38F803FE489038C0007E4849133E49C7120E001F15064991C7FC485AA2485AA4485AAE6C
7EA46C7EA26C7E6D1403000F5D6D6C5B6C6D133F6C9039F801FF806C90B6FC7E7F011FEC
FE00010714F8010114E0D9001F90C7FC29347CB232>67 D<007FB61280B712C0A5168001
E0C8FCAE90B512FE81A55D01E0C8FCAE90B612C016E0A66C15C0233279B12E>69
D<007FB6FCB71280A5160001E0C8FCAE90B512F881A55D01E0C8FCB3A36C5A213279B12C
>I<EA7FC0487EB3B3A690B512FC15FEA56C14FC1F3279B12A>76
D<EC3FFC0103B512C0010F14F0013F14FC90B7FC48D9F00F138048D9C00313C04890C713
E04848EC7FF049143F001F16F849141F003F16FC49140FA2007F16FEA2491407A200FF16
FFAE007F16FE6D140FA46C6CEC1FFCA26C6CEC3FF8A26C6CEC7FF06D14FF6CD9C00313E0
6CD9F00F13C06C90B612806C1600013F14FC6D5C010314C09026003FFCC7FC30347CB239
>79 D<007FB512C0B612F815FEEDFF8016C016E0D9E00313F0EC007FED3FF8151FA216FC
A2150FA5151FA216F8153FA2ED7FF0913803FFE090B6FC16C016005D15F001E0C8FCB36C
5A263279B132>I<007FB512C0B612F815FF168016C016E0D9E00113F09138007FF8153F
151F16FCA2150FA4151FA216F8153FED7FF0EC01FF90B612E016C0160015FC15E09038E0
7FF0143F81141F81140F816E7EA26E1380A26E13C0A26E13E0A2ED7FF0153F16F8ED1FFC
A2ED0FFEA26C48EB07FC273279B132>82 D<EB07FF017F13E048B512F84814FE48ECFF80
5A5AA2263FFC0113009038F0003F497F484813078192C7FCA37F7FEA3FFCEBFFC014FC6C
EBFFC06C8015F86C806C80C6806D1480011F14C01301D9001F13E014019138007FF0153F
A2151FA312601278007C143F007F15E001C0137F39FFFC01FF90B612C01680A2003F1500
000F5C000314F8C66C13E0010790C7FC24347DB22C>I<007FB712F8B812FCA56C16F8C7
D83FF8C7FCB3B3A66E5A2E327DB135>I<EB1FFC90B51280000314E04814F04814F89038
E00FFC138090380007FE120E120CC7FCA3EB0FFF90B5FC1203000F1307EA1FF8EA3FF0EA
7FE0EAFFC0A5EBE00F007F131FEBF07F6CB5FC6C13F76C13E76C13873901FC03FC1F217E
A026>97 D<EA7F80487EB0EBC1FE9038C7FF8001DF13E090B512F015F8EBF81F9038E00F
FC9038C007FEA3140315FFAB15FE1407A215FCEBE00F9038F03FF890B512F015E001DF13
C001CF1300387F83FC20327CB128>I<EC01FEEC03FFB0EB3FC33801FFF34813FB4890B5
FC5A381FFC0F383FF00313E0127FA213C012FFAB127F13E0A2123F6D5A381FF81F6CB6FC
7E6C13FB6C13E339003F81FE20327DB128>100 D<EB0FFC90387FFF8048B512E0000714
F04814F8381FFC0F9038F003FCD83FE013FE007F130113C015FF00FF7FA390B6FCA315FE
0180C7FC7FA2127FA27F003F14066D130E6C6C133E390FFE01FE90B5FC12036C14F86C6C
13E0903807FE0020217EA025>I<90391FF801E090B5EA0FF0000314FF5A4814F0D9F81F
130048486C7EEBE007003F80A7001F5CEBF00F6C6C485A90B5FC6C5C5D000691C7FC380E
1FF890C9FC120F487E90B512C06C14FC81EDFF806C15C0A2001F15E05A3A7F80007FF048
C7121F150FA46C6CEB1FE06D133FD83FF0EBFFC06CB612806C15006C5C000114F8D8001F
138024307FA027>103 D<EA7F80487EB0EC7F809038C1FFE001C313F001CF13F801DF13
FCEBDE0F9038F807FE13F013E0A213C0B3A4397F8003FC1F327CB128>I<EA7FC0EAFFE0
A9EA7FC0C7FCA7EA3FC0EA7FE0B3ADEA3FC00B337DB213>I<EA7F80EAFFC0B3B3ACEA7F
800A327CB113>108 D<277F803FC013FF28FFC1FFF00713C001C36D4813E001C76D4813
F001CF6D4813F8D9DE07EB781F903BF803FFE00FFC01F014C001E01480A201C01400B3A4
6C486C48EB07F836217CA03F>I<397F807F8039FFC1FFE001C313F001CF13F801DF13FC
EBDE0F9038F807FE13F013E0A213C0B3A4397F8003FC1F217CA028>I<EB0FFC90B512C0
000314F048804880391FFC0FFE393FF003FF497E007F1580A2497EA200FF15C0AA007F15
806D5AA26C6C481300A2391FFC0FFE6CB55A6C5C6C5CC614C0D91FFEC7FC22217EA027>
I<387F81FE39FFC7FF8001DF13E090B512F015F8EBF83F9038E00FFC01C013FE1407A3EC
03FFABEC07FEA3EC0FFCEBE01F9038F03FF890B512F015E001DF13C001CF1300EBC3FC01
C0C7FCAD6C5A202F7CA028>I<007F137838FF81F813831387138F139F13BF1480EBFC00
5B5B5BA25BB36C5A15217CA01B>114 D<EA03FC487EA8387FFFFEB6FCA36C5BD807FEC7
FCB3A25C5C9038FF0F806C13FF15006C5B6C13F8EB7F80192A7FA91D>116
D<397F8003FC39FFC007FEB3A5140FA2141F127FEBE07F383FFFF76C13E76C13870003EB
03FC1F217CA028>I<00FE14FE38FF80011403A213C0007FEB07FCA213E0003FEB0FF8A2
13F0001FEB1FF0A3390FF83FE0A313FC0007EB7FC0A213FE0003EBFF80A290B5FC6C1400
A36C5BA46D5A6D5A1F217EA024>I E end
%%EndProlog
%%BeginSetup
%%Feature: *Resolution 300dpi
TeXDict begin
%%PaperSize: a4
%%EndSetup
%%Page: 1 1
1 0 bop 584 349 a Ff(CALL)26 b(F)n(OR)g(P)-7 b(APERS)78
456 y Fe(Sp)r(ecial)23 b(Issue)f(of)f(the)i(Journal)f(of)f(Automated)h
(Reasoning)g(\(JAR\))887 516 y(on)55 612 y Ff(Computer)k(Algeb)n(ra)f
(and)h(Automated)f(Theo)n(rem)g(Proving)464 731 y Fd(Edito)o(rs:)c
(Deepak)16 b(Kapur)f(and)i(Dongming)h(W)o(ang)147 952
y Fc(Computer)23 b(algeb)o(ra)i(\(CA\))f(metho)q(ds)g(a)o(re)f(among)i
(some)e(of)i(the)e(most)h(p)q(o)o(w)o(erful)f(ones)50
1012 y(develop)q(ed)c(fo)o(r)g(automated)f(theo)o(rem)f(p)o(roving)j
(\(A)l(TP\))f(in)h(several)f(sp)q(ecialized)h(mathematical)50
1072 y(domains.)j(T)l(ypical)18 b(examples)f(a)o(re)f(algeb)o(raic)i
(metho)q(ds)e(fo)o(r)g(A)l(TP)h(in)g(geometry)l(,)f(which)h(require)50
1132 y(complex)d(and)g(heavy)g(p)q(olynomial)j(op)q(erations.)j(A)l(TP)
15 b(techniques)d(a)o(re)h(b)q(eing)i(inco)o(rp)q(o)o(rated)e(into)50
1192 y(the)19 b(design)g(and)h(implementation)g(of)g(current)d(CA)j
(systems.)30 b(Resea)o(rch)18 b(p)o(rojects)g(have)i(b)q(een)50
1253 y(explo)o(ring)d(the)f(co)q(op)q(eration,)h(combination)g(and)g
(integration)f(of)h(CA)g(and)f(A)l(TP)h(systems.)147
1313 y(This)k(sp)q(ecial)f(issue)g(is)g(devoted)g(to)g(rep)q(o)o(rting)
f(signi\014cant)i(resea)o(rch)d(developments)h(and)50
1373 y(to)h(motivating)i(further)d(investigations)j(on)e(the)g
(interaction)h(of)f(CA)h(and)g(A)l(TP)g(\(systems\))e(in)50
1433 y(resea)o(rch,)j(education)h(and)g(industrial)h(applications.)42
b(Original)25 b(resea)o(rch)c(pap)q(ers)h(describing)50
1493 y(recent)13 b(advances)j(and)g(new)f(insights)g(on)h(all)h(asp)q
(ects)d(of)i(coupling)g(CA)g(and)g(A)l(TP)g(a)o(re)e(solicited.)50
1554 y(Sp)q(eci\014c)i(topics)g(of)h(interest)d(include)j(\(but)f(a)o
(re)f(not)i(limited)f(to\):)122 1668 y Fb(\017)25 b Fc(Inco)o(rp)q(o)o
(rating)16 b(A)l(TP)h(Mechanisms)f(and)h(T)l(o)q(ols)g(into)g(CA)g
(Systems,)122 1769 y Fb(\017)25 b Fc(Combining)18 b(CA)e(and)h(A)l(TP)g
(Systems,)122 1871 y Fb(\017)25 b Fc(Applications)17
b(of)g(Combined)g(Systems.)147 1985 y(The)23 b(deadline)h(fo)o(r)f
(submission)g(is)h Fa(Ma)n(y)i(15,)j(1996)p Fc(.)43 b(All)25
b(submitted)d(pap)q(ers)g(will)j(b)q(e)50 2045 y(refereed)20
b(acco)o(rding)i(to)g(the)g(JAR)g(refereeing)f(p)o(ro)q(cess.)37
b(The)22 b(sp)q(ecial)h(issue)f(is)g(exp)q(ected)f(to)50
2106 y(app)q(ea)o(r)16 b(in)h(1997.)147 2201 y(Autho)o(rs)f(a)o(re)f
(invited)i(to)f(submit)g(3)h(copies)f(of)g(their)g(manuscripts)f(to)75
2307 y(Prof.)g(Deepak)h(Kapur)452 b(o)o(r)179 b(Dr.)16
b(Dongming)h(W)o(ang)75 2367 y(Depa)o(rtment)d(of)i(Computer)g(Science)
398 b(LIFIA{IMA)o(G{CNRS)75 2427 y(State)15 b(Universit)o(y)i(of)f(New)
g(Y)l(o)o(rk)487 b(46,)17 b(avenue)f(F)o(\023)-23 b(elix)17
b(Viallet)75 2488 y(Albany)l(,)g(NY)g(12222)710 b(38031)19
b(Grenoble)c(Cedex)75 2548 y(USA)986 b(F)o(rance)75 2633
y(F)o(ax:)21 b(\(1\))c(518)g(442)g(5638)618 b(F)o(ax:)22
b(\(33\))17 b(76)g(57)g(46)g(02)75 2693 y(E-mail:)22
b(k)o(apur@cs.albany)l(.edu)501 b(E-mail:)23 b(w)o(ang@li\014a.imag.fr)
p eop
%%Trailer
end
userdict /end-hook known{end-hook}if
%%EOF