%PDF-1.3 % 1 0 obj << /Producer (BaKoMa TeX 6.10 4225P1698/104784677) /Creator (Alexei A. Morozov) /CreationDate (D:20070730231617) /Title ( O p e r a t i o n a l A p p r o a c h t o t h e M o d i f i e\ d R e a s o n i n g , B a s e d o n t h e C o n c e p t o f\ R e p e a t e d P r o v i n g a n d L o g i c a l A c t o r s\ ) /Author ( A l e x e i A . M o r o z o v , I n s t i t u t e o f R a d\ i o E n g i n e e r i n g a n d E l e c t r o n i c s R A S) /Subject ( C I C L O P S 2 0 0 7 , S e p t e m b e r 8 , P o r t o , P\ o r t u g a l) /Keywords ( l o g i c p r o g r a m m i n g , r e p e a t e d p r o v i n g\ , l o g i c a l a c t o r s , o p e r a t i o n a l s e m a n t\ i c s , t r a n s i t i o n s y s t e m , a b s t r a c t m a c\ h i n e , A c t o r P r o l o g) /ModDate (D:20070730231657+04'00') >> endobj 2 0 obj [ /PDF /Text /ImageB /ImageC ] endobj 3 0 obj << /Pages 4 0 R /Outlines 138 0 R /Dests 139 0 R /Type /Catalog /Page 1 /View [ /Fit ] /URI << /Base ()>> /PageMode /UseNone /ViewerPreferences << >> /OpenAction 152 0 R >> endobj 4 0 obj << /Kids [ 14 0 R 33 0 R 38 0 R 50 0 R 57 0 R 64 0 R 69 0 R 80 0 R 83 0 R 90 0 R 93 0 R 96 0 R 100 0 R 103 0 R 106 0 R ] /Count 15 /Type /Pages /MediaBox [ 0 0 595 842 ] >> endobj 5 0 obj << /Type /Encoding /Differences [ 0 /Gamma /Delta /Theta /Lambda /Xi /Pi /Sigma /Upsilon /Phi /Psi /Omega /ff /fi /fl /ffi /ffl /dotlessi /dotlessj /grave /acute /caron /breve /macron /ring /cedilla /germandbls /ae /oe /oslash /AE /OE /Oslash /polishlcross /exclam /quotedblright /numbersign /dollar /percent /ampersand /quoteright /parenleft /parenright /asterisk /plus /comma /hyphen /period /slash /zero /one /two /three /four /five /six /seven /eight /nine /colon /semicolon /exclamdown /equal /questiondown /question /at /A /B /C /D /E /F /G /H /I /J /K /L /M /N /O /P /Q /R /S /T /U /V /W /X /Y /Z /bracketleft /quotedblleft /bracketright /circumflex /dotaccent /quoteleft /a /b /c /d /e /f /g /h /i /j /k /l /m /n /o /p /q /r /s /t /u /v /w /x /y /z /endash /emdash /hungarumlaut /tilde /dieresis 160 /hardspace /Gamma /Delta /Theta /Lambda /Xi /Pi /Sigma /Upsilon /Phi /Psi 173 /Omega /ff /fi /fl /ffi /ffl /dotlessi /dotlessj /grave /acute /caron /breve /macron /ring /cedilla /germandbls /ae /oe /oslash /AE /OE /Oslash /polishlcross /dieresis ] >> endobj 6 0 obj << /Type /Font /Subtype /Type1 /Name /F0 /BaseFont /FXXFVU+TeX-cmbx12 /Encoding 5 0 R /ToUnicode 116 0 R /FirstChar 0 /LastChar 196 /Widths [ 675 937 875 787 750 879 812 875 812 875 812 656 625 625 937 937 312 343 562 562 562 562 562 849 500 574 812 875 562 1018 1143 875 312 342 581 937 562 937 875 312 437 437 562 875 312 375 312 562 562 562 562 562 562 562 562 562 562 562 312 312 342 875 531 531 875 849 799 812 862 738 707 884 879 418 581 880 675 1067 879 844 768 844 839 625 782 864 849 1162 849 849 687 312 581 312 562 312 312 546 625 500 625 513 343 562 625 312 343 593 312 937 625 562 625 593 459 443 437 625 593 812 593 593 500 562 1125 562 562 562 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 675 937 875 787 750 879 812 875 812 875 0 0 812 656 625 625 937 937 312 343 562 562 562 562 562 849 500 574 812 875 562 1018 1143 875 312 562 ] /FontDescriptor << /Type /FontDescriptor /Flags 4 /ItalicAngle 0 /FontName /FXXFVU+TeX-cmbx12 /FontBBox [ -57 -250 1139 751 ] /FontFile3 137 0 R /CapHeight 562 /XHeight 426 /Ascent 751 /Descent -250 /StemV 108 /StemH 47 >> >> endobj 7 0 obj << /Type /Font /Subtype /Type1 /Name /F1 /BaseFont /AJFRFO+TeX-cmr10 /Encoding 5 0 R /ToUnicode 116 0 R /FirstChar 0 /LastChar 196 /Widths [ 625 833 777 694 666 750 722 777 722 777 722 583 555 555 833 833 277 305 500 500 500 500 500 750 444 500 722 777 500 902 1013 777 277 277 500 833 500 833 777 277 388 388 500 777 277 333 277 500 500 500 500 500 500 500 500 500 500 500 277 277 277 777 472 472 777 750 708 722 763 680 652 784 750 361 513 777 625 916 750 777 680 777 736 555 722 750 750 1027 750 750 611 277 500 277 500 277 277 500 555 444 555 444 305 500 555 277 305 527 277 833 555 500 555 527 391 394 388 555 527 722 527 527 444 500 1000 500 500 500 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 625 833 777 694 666 750 722 777 722 777 0 0 722 583 555 555 833 833 277 305 500 500 500 500 500 750 444 500 722 777 500 902 1013 777 277 500 ] /FontDescriptor << /Type /FontDescriptor /Flags 4 /ItalicAngle 0 /FontName /AJFRFO+TeX-cmr10 /FontBBox [ -44 -250 1009 750 ] /FontFile3 136 0 R /CapHeight 562 /XHeight 426 /Ascent 750 /Descent -250 /StemV 70 /StemH 35 >> >> endobj 8 0 obj << /Type /Font /Subtype /Type1 /Name /F2 /BaseFont /KKOBVV+TeX-cmr9 /Encoding 5 0 R /ToUnicode 116 0 R /FirstChar 0 /LastChar 196 /Widths [ 642 856 799 713 685 770 742 799 742 799 742 599 570 570 856 856 285 314 513 513 513 513 513 770 456 513 742 799 513 927 1041 799 285 285 513 856 513 856 799 285 399 399 513 799 285 342 285 513 513 513 513 513 513 513 513 513 513 513 285 285 285 799 485 485 799 770 727 742 785 699 670 806 770 370 528 799 642 941 770 799 699 799 756 570 742 770 770 1056 770 770 628 285 513 285 513 285 285 513 570 456 570 457 314 513 570 285 314 542 285 856 570 513 570 542 401 405 399 570 542 742 542 542 456 513 1027 513 513 513 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 642 856 799 713 685 770 742 799 742 799 0 0 742 599 570 570 856 856 285 314 513 513 513 513 513 770 456 513 742 799 513 927 1041 799 285 513 ] /FontDescriptor << /Type /FontDescriptor /Flags 4 /ItalicAngle 0 /FontName /KKOBVV+TeX-cmr9 /FontBBox [ -43 -251 1036 750 ] /FontFile3 135 0 R /CapHeight 562 /XHeight 426 /Ascent 750 /Descent -251 /StemV 75 /StemH 35 >> >> endobj 9 0 obj << /Type /Encoding /Differences [ 0 /Gamma /Delta /Theta /Lambda /Xi /Pi /Sigma /Upsilon /Phi /Psi /Omega /arrowup /arrowdown /quotesingle /exclamdown /questiondown /dotlessi /dotlessj /grave /acute /caron /breve /macron /ring /cedilla /germandbls /ae /oe /oslash /AE /OE /Oslash /visiblespace /exclam /quotedbl /numbersign /dollar /percent /ampersand /quoteright /parenleft /parenright /asterisk /plus /comma /hyphen /period /slash /zero /one /two /three /four /five /six /seven /eight /nine /colon /semicolon /less /equal /greater /question /at /A /B /C /D /E /F /G /H /I /J /K /L /M /N /O /P /Q /R /S /T /U /V /W /X /Y /Z /bracketleft /backslash /bracketright /asciicircum /underscore /quoteleft /a /b /c /d /e /f /g /h /i /j /k /l /m /n /o /p /q /r /s /t /u /v /w /x /y /z /braceleft /bar /braceright /asciitilde /dieresis 160 /hardspace /Gamma /Delta /Theta /Lambda /Xi /Pi /Sigma /Upsilon /Phi /Psi 173 /Omega /arrowup /arrowdown /quotesingle /exclamdown /questiondown /dotlessi /dotlessj /grave /acute /caron /breve /macron /ring /cedilla /germandbls /ae /oe /oslash /AE /OE /Oslash /visiblespace /dieresis ] >> endobj 10 0 obj << /Type /Font /Subtype /Type1 /Name /F3 /BaseFont /HXVFTS+TeX-cmtt9 /Encoding 9 0 R /ToUnicode 115 0 R /FirstChar 0 /LastChar 196 /Widths [ 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 524 524 524 524 524 524 524 524 524 524 0 0 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 524 ] /FontDescriptor << /Type /FontDescriptor /Flags 4 /ItalicAngle 0 /FontName /HXVFTS+TeX-cmtt9 /FontBBox [ -9 -233 544 700 ] /FontFile3 134 0 R /CapHeight 562 /XHeight 426 /Ascent 700 /Descent -233 /StemV 78 /StemH 69 >> >> endobj 11 0 obj << /Type /Font /Subtype /Type1 /Name /F4 /BaseFont /HLEIUL+TeX-cmbx9 /Encoding 5 0 R /ToUnicode 116 0 R /FirstChar 0 /LastChar 196 /Widths [ 710 986 920 827 788 924 854 920 854 920 854 690 657 657 986 986 328 361 591 591 591 591 591 892 525 616 854 920 591 1070 1202 920 328 360 617 986 591 986 920 328 460 460 591 920 328 394 328 591 591 591 591 591 591 591 591 591 591 591 328 328 360 920 558 558 920 892 840 854 906 776 743 929 924 446 610 925 710 1121 924 888 808 888 886 657 823 908 892 1221 892 892 723 328 617 328 591 328 328 575 657 525 657 542 361 591 657 328 361 624 328 986 657 591 657 624 488 466 460 657 624 854 624 624 525 591 1183 591 591 591 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 710 986 920 827 788 924 854 920 854 920 0 0 854 690 657 657 986 986 328 361 591 591 591 591 591 892 525 616 854 920 591 1070 1202 920 328 591 ] /FontDescriptor << /Type /FontDescriptor /Flags 4 /ItalicAngle 0 /FontName /HLEIUL+TeX-cmbx9 /FontBBox [ -62 -250 1195 750 ] /FontFile3 133 0 R /CapHeight 562 /XHeight 426 /Ascent 750 /Descent -250 /StemV 115 /StemH 53 >> >> endobj 12 0 obj << /Length 2153 /Filter /FlateDecode >> stream xڥMo6^!Gh\GӺaް7uV9v&_?R;M "i(~&^E8ee@C:M