Treffer: Efficient rewriting of operations on finite structures in ACL2
Title:
Efficient rewriting of operations on finite structures in ACL2
Authors:
Source:
3rd international workshop on the ACL2 theorem prover and its applications (Grenoble, 8-9 April 2002). :141-150
Publication Year:
2002
Physical Description:
print, 4 ref
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences et techniques communes, Sciences and techniques of general use, Mathematiques, Mathematics, Logique mathématique, fondements, théorie des ensembles, Mathematical logic, foundations, set theory, Logique et fondements, Logic and foundations, Théorie de la preuve et mathématiques constructives, Proof theory and constructive mathematics, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Informatique théorique, Theoretical computing, Théorie programmation, Programming theory, Intelligence artificielle, Artificial intelligence, Résolution de problèmes, jeux, Problem solving, game playing, Démonstration théorème, Theorem proving, Demostración teorema, Langage programmation, Programming language, Lenguaje programación, Programme concurrent, Concurrent program, Programa competidor, Réécriture, Rewriting, Reescritura, Structure donnée, Data structure, Estructura datos, Structure programme, Program structure, Estructura programa, ACL2 logic, Logique calcul
Document Type:
Konferenz
Conference Paper
File Description:
text
Language:
English
Author Affiliations:
Advanced Micro Devices 5900 E. Ben White Blvd., Austin, Texas, 78741, United States
Rights:
Copyright 2002 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Mathematics
Mathematics
Accession Number:
edscal.14198207
Database:
PASCAL Archive
Weitere Informationen
We give a useful set of unconditional rewrite rules for reasoning about record structures, which are essentially finite functions. The problem, then, is to define functions for which these rules are true and then prove the rules. We begin with a series of definitions that attempt to satisfy these rules but fall short for various reasons. Then we give two solutions, one of which generalizes to other finite structures. The definitions of our access and update functions are somewhat subtle, complex, and ineffecient, but they return the expected values and the theorems exported are elegant and efficient for automatic, unconditional rewriting.