D:\sbornik\...\Tigran.DVI


Mathematical Problems of Computer Science 24, 2005, 107{119.

Analysis of Case Splitting in an Ar ithmetical System

Tig r a n M. Ga lo ya n

Institue for Informatics and Automation Problems of NAS of RA

e-mail tiger galo@yahoo.com

Abstract

Investigations in this paper concern the analysis of case splitting [(: A ! B) !
(A ! B) ! B] in an arithmetical system. It is shown that the case splitting can
be done according to a thicker class of formulas (quanti¯er-free formulas) instead of
decidable formulas. The latter includes the class of quanti¯er-free formulas. Some
approaches to the case splitting, promoted by other authors, have been investigated,
and some corrections concerning the selection of quanti¯er-free formulas instead of
decidable formulas have been done. According to these corrections, a new derivation
of case splitting is suggested.

Refer ences

[1 ] S . C. K le e n e , In t r o d u c t io n t o Me t a m a t h e m a t ic s . B ib lio t e c h a Ma t h e m a t ic a , 1 9 5 7 .

[2 ] W ilfr ie d B u c h h o lz , U lr ic h B e r g e r a n d H e lm u t S c h wic h t e n b e r g , R e ¯ n e d P r o g r a m E xt r a c -
t io n fr o m Cla s s ic a l P r o o fs . In s t it u t e MITTA G-L E FFL E R , t h e R o ya l S we d is h A c a d e m y
o f S c ie n c e s , 2 0 0 0 .

[3 ] U lr ic h B e r g e r a n d H e lm u t S c h wic h t e n b e r g . P r o g r a m D e ve lo p m e n t b y P r o o f Tr a n s fo r -
m a t io n . In H . S c h wic h t e n b e r g , e d it o r , P roof and Computation, vo lu m e 1 3 9 o f Series F :
Computer and Systems Sciences, p a g e s 1 -4 5 . N A TO A d va n c e d S t u d y In s t it u t e , In t e r -
n a t io n a l S u m m e r S c h o o l h e ld in Ma r kt o b e r d o r f, Ge r m a n y, Ju ly 2 0 - A u g u s t 1 , 1 9 9 3 ,
1 9 9 5 .

¸»åù»ñÇ ïñáÑÙ³Ý í»ñÉáõÍáõÃÛáõÝÁ Ãí³µ³Ý³Ï³Ý ѳٳϳñ·áõÙ

î. ¶³ÉáÛ³Ý

²Ù÷á÷áõÙ

àõëáõÙݳëÇñáõÃÛáõÝÝ»ñÁ ÝíÇñí³Í »Ý ¹»åù»ñÇ ïñáÑÙ³Ý [( : A ! B ) ! ( A ! B ) !
B] í»ñÉáõÍáõÃÛ³ÝÁ Ãí³µ³Ý³Ï³Ý ѳٳϳñ·áõÙ£ òáõÛó ¿ ïñí»É, áñ ¹»åù»ñÇ ïñáÑáõÙÁ
µ³í³Ï³Ý ¿ ϳï³ñ»É ѳٳӳÛÝ µ³Ý³Ó¨»ñÇ ³í»ÉÇ Ý»Õ ¹³ëǪ ùí³ÝïáñÝ»ñÇó ³½³ï
µ³Ý³Ó¨»ñÇ, áñáß»ÉÇ µ³Ý³Ó¨»ñÇ ¹³ëÇ ÷á˳ñ»Ý£ ì»ñçÇÝë ³í»ÉÇ É³ÛÝ ¹³ë ¿ ¨ Áݹ·ñÏáõÙ

1 0 7



1 0 8 Analysis of Case Splitting in an Arithmetical System

¿ ùí³ÝïáñÝ»ñÇó ³½³ï µ³Ý³Ó¨»ñÇ ¹³ëÁ£ àõëáõÙݳëÇñí»É »Ý ݳ¨ ³ÛÉ Ñ»ÕÇݳÏÝ»ñÇ
Ùáï»óáõÙÝ»ñÁ ¹»åù»ñÇ ïñáÑÙ³ÝÁ ¨ ϳï³ñí»É »Ý áñáß ×ß·ñïáõÙÝ»ñ ϳåí³Í áñáß»ÉÇ
µ³Ý³Ó¨Ç ÷á˳ñÇÝÙ³ÝÁ ùí³ÝïáñÝ»ñÇó ³½³ï µ³Ý³Ó¨áí£ Ð³Ù³Ó³ÛÝ ³Ûë ³Ù»ÝÇ
³é³ç³ñÏí»É ¿ ¹»åù»ñÇ ïñáÑÙ³Ý Ýáñ ³ñï³ÍáõÙ£