scieee Science in your language
[en] (orig)

Formalizing Rewriting in the ACL2 Theorem Prover

Abstract

We present an application of the ACL2 theorem prover to formalize and reason about rewrite systems theory. This can be seen as a first approach to apply formal methods, using ACL2, to the design of symbolic computation systems, since the notion of rewriting or simplification is ubiquitous in such systems. We concentrate here on formalization and representation aspects of abstract reduction and term rewriting systems, using the first-order, quantifier-free ACL2 logic based on Common Lisp.

Read accessible full text

Formalizing Rewriting in the ACL2 Theorem Prover

Author: Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús
Publisher: Springer
Year: 2000
DOI: 10.1007/3-540-44990-6_7
Source: https://idus.us.es/bitstreams/bca2d192-28c1-4675-9b68-bd8c00c5a37c/download
     


      
  




        
       
  ! " #$%$&  

'     ( )& (  
*   +  ,  ( -(  + 
   (    (   )&  ( .
  +     (   , 
  +/  (  '  (  .
*     +   
,   ( . /. )&  +
  )
  
                  !
" #   $   %" %& '  
'  % " "     # $  
"    !   "  $  $  
 "  %" #$ "% #  (")
""   *+,   "-
 !  $      " " # %"  
- .  !    ,% /0 0   /
%-  !    ""   # $  ""
- . %" ## "  +%  " #   
(/"-
 "     " # #"#  % "
#0  ""  $      ,"
 "  "     %- 1    
    "0    "  %"$  "
& "0      " ", $ 2  
 $ /# $ " $ 2   " / 
 /#  3  ," 456  4768-

-( ,0 ( +   + 1"!2 3 4 3567.%%68.%#.%# 
3567.$9#:
9  !    ""     $   
0   $ #0 ,$ ""     " 
%"$  " %"-   % #0 ""  
 %"  % $%  $ # $ "  $
"% :0;        %"-
       !  3 /0 
0 $ 2    #$ -8  $     "
  "% # # "- <      "
  $  "      - = 
       " - . " 
"  #$   $ 

-
   
 $'% $     ! " #   - . $  
    !  4>6- . $ " $   !    !
) "  4?6-     "  /   (/"
    !  $    4@6-
 !    "   # "" - .
 !    /0 0   /% $  
# $  "" - . %,  "    "" 
4A56 3  "     "   8- . 
 ,"        "$     
 % -          /%
 - +% 
  
   0 3

8  "  ," %   ,   "  
 "   #  - .    
    $%  0- . %   # 0
    

¼
  "     "$  # $%  


  

- 1 "     

  
  "  $%  

¼
-
<    0    "" 3

8        %"$ $% ," 
 "  #    3  %    
 #  "     $ ,$8- < 


   

  $  #       
  "   " ,"- .  % 0


 $     #$  
   -  #      
 "    & " $  
 $    %"$    #  "  -
.  ! " #   $% (/" $  $  $%
"#- . "  /  $%#  "0 
- 9"0   "$     "% "
    #% # $%  - . ""

   "      "     - .
" #  "     

 #  
      %"- #       %" 
#- B%  #     $%  %"   0
"- .      # $%  ""  0
  $/   - .      " &  %
  C   "  $"      
#  0  #  $% "   $    -
      
.  #     $   0 "
 %     -  "   $   4A6-

 
 "%  $% 

0   

-
  









 #%  #   %""
  ',##    /# - . 
  0       

-"

 
 
3

8  





-%



 2$ 3 



8   ,

 







-%










-
 "   % % $      ,
 / " "  /#$ 2-     
 
 #%  /# $ 2  2$-  /#
  %

&  
  
 











-
<       %    " "
 $  /#- <     

3-- #% "
  " "  


8




C


D


-E# " "
 "$  %

 $   /# 


 $        /%  " "-
 "   %  "&    


3

8     0  /

¼


½


¾


-
1$#%#%     "- .  
%  $       "- <    /#
  %
 
&  
  






 



-
.    
 
-
1 "%      0   

3
 
8
0  "   #  

     %"$ 

    #$- <  , 

   "

D

-
.    $%    /

 0  &




  ,

D



  $

  #$ 

3

$8  

3

8   $" 



 $
"

$%   $"

3

8$%

3

8- .     
  # $ $    $ # 


D

D

C





-
. " $%#% / % 0 $%  ,"

 


 "  % '- . "   
 /

D

"    $  $ #  




 $
 
-
  
3.98      -
F  

 %    / 3/ ,"8


  "  %"-
  '  $  0  " .9& 2$%
%  $    0 "$    " 
 

   "  "    #- .
 

   .9   % ' C      2
$- .   %  " .9   $  %&
     #%     "" " "- <  .9

     C " "       $
      / % 

 2  / 
  "  - .   $   


3 4A6  8-
<  /  $   "       !
     "   " #-       
   $ :#;  " :"% #   !;-
     
1 0 "   $      ! 
 "%  0 "  $% $   


   - (# 



 " "   
$



   

 $ "

$% % " 
 " 

- <  " $ "   #
    $%   #  "     
  $ 2 " 
 

-   ,"
/ & "     0 "   
  $ 2  $%    3  $" 8 
/ 3  8   $ 3 " $8-
1   %    $   % "- .  
"    "  &  $ $%   
  

 %      "- %   "
  &  "  " " /   
   %     %     
 "       #  , 

 3

8-
. $ #     "    $ 
   !   % 0 &





- .  $    


3  
 "          8&

 ! " "  ! " "  !" ""

 #
  !"  !  !""""
 
   !""   ! """"
"
. 0   #%

      
   % 0- .  " " $ #  ,"
 "" /"  #%   0&    
3 ,"   ' '   %8  " %
  $   

-.   #% $ "
 "    !-       
 $ $  #%  - 1     
 &  "  " " %    $
$ 2  $- 1     # & #
% 
 $   /# -     %
  0     %  '   
%  # # # "  (") ""   
-
.    "   






#  $ 0     "
  ," " $ #    0- +% 
  $  $    $  % ,  
  3      / 8-
     
=   #    
!     0




 #    "   /  

D

¼


½


¾




D

- .   $%  
$%
0  0 A-
$% ! & "




   2% 
!


&
-

½
  /
         

  0&
#


3 " 8

3    8 

-
.   2%  " /#  $    $ 

-
 

3 0 $%

8    "  $
%  38      3    $%

8-
  %   '  $ 0   
  "     3$ !-!  !-@8-      
0 3" 8         3
 

 
8&
'
     "






%&
     "







-
 !"    
 $   "  #    #% 
 "    $- B%    $  
½
   ,(    ( )& 

     
  
            

 
     
    
      
    
    
     
        
     
 
    /
"  0     %&    
 C  #%    ,  /##% - 9   !
  /0  , /0   "   $  
 $%9"  
%&
- . 
 $  "   $ "  "   &   
"   #% "  ,     /# $
"- .    # $%  39"8 

3
    "  %%8- E  0  
 "  

   0 ! "
"
-
. 
$%
  " "  /- (   "
"   "
!
   "
 !"
&
  !"
 !  !"""
 $% ! &"
$  !"  &"""
. # $%     "   
  #
$%
  "   "  
/#      - 9 0 ! "
"
-     " ""       
/# $ "- (     ,  "
  9" 
'
30 "8
     2%  /#- . "  #
%  "  "  - 9  $   -
       

        !  
   !  
"""""
 
   
    
      
"""""
 
#  ! 
   
      ! 
 ! $  
 %!   

      !   ! 
  
 
       &  
 
       
 
((.   *  +
#  $   %   
  
  
  

 #% "% $   ""
"-       $   ! $ 
  ""&     

  C  ,
 

&







3

8

3

8 

  
   3,"   8- <  !     # 
%  /"   $     "$%   #
-     

 $ 0   ! 
  "
"
 0 @- 9 %   

¼
 "  
 !   "  "    ","  %  
   $  - /%  " C "
 " - (#     

¼
   
  ,   
  " "    $
      ##-
< "
"
 0 @   0       % '
    -  '  % ,  "
  ' %  

      
"""
 %
 (  
    ()    
 %
 
          
 ! '      

       
!   &  
""""
 
  & 
      & 
  
   
 
        
      
  
    
% 
  & 

 & 
  $  
 
 & 
  & 
 
 *%
   
    
  
   
 
;,< 
       ##&    % ' C  #%  
       /##%  - . #%   # $%
% 0 
'
-    %
"     ""&       
%          3 8- .  
 

#% 0    2%  %
    0&  #% "
!
  

 

 $   

$  "  
!
   

-
.    (") ""     3 4A68 
' $%    $    - .  
 $   ! C "       $    
#  4G6- <  " #    
    %$% 0  
%&
 #   #% 


%& "
  /#
#
% -
.   0  #% %
'
3
     $ $%  /#   # $%

'
8       - 9 0  "
"
 0 @-
<          $%  "  

%&
   "- . "   C  
     " "   

 
       

- .  $    
"     - . "

  
 " ##       

 0  $  
 


-   # !   " ,
             
 3  $   8- 1
%&
 " 
 #% %     %   /##%  - 9
"
"
 0 @-
(  #   :""; 
%&
 #  "    "  ,"   # $
- . "   

- =$%   
  % '     $  %  $% 
 "    #   # $ 
 "    - (" '  # $% 
""     $  "# "-
    
 0   #   #%  "  
- .  #  $   #%    
"-   " 2 ,"  $      "
  $  "    !-