Presentation
Formal Verification of Molecular Computational Models in ACL2: A Case Study
Author/s | Martín Mateos, Francisco Jesús
Alonso Jiménez, José Antonio Hidalgo Doblado, María José Ruiz Reina, José Luis |
Department | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial |
Publication Date | 2003 |
Deposit Date | 2019-05-10 |
Published in |
|
ISBN/ISSN | 978-3-540-22218-7 0302-9743 |
Abstract | Theorem proving is a classical AI problem with a broad range
of applications. Since its complexity is exponential in the size of the
problem, many methods to parallelize the process has been proposed.
One of these ... Theorem proving is a classical AI problem with a broad range of applications. Since its complexity is exponential in the size of the problem, many methods to parallelize the process has been proposed. One of these approaches is based on the massive parallelism of molecular reactions. ACL2 is an automated theorem prover especially adequate for algorithm verification. In this paper we present an ACL2 formalization of a molecular computational model: Adleman’s restricted model. As an application of this model, an implementation of Lipton’s experiment solving SAT is described. We use ACL2 to make a formal proof of the completeness and soundness properties of this implementation. |
Project ID. | TIC2000-1368-C03-02 |
Citation | Martín Mateos, F.J., Alonso Jiménez, J.A., Hidalgo Doblado, M.J. y Ruiz Reina, J.L. (2003). Formal Verification of Molecular Computational Models in ACL2: A Case Study. En TTIA 2003: 5th Conference on Technology Transfer (344-353), San Sebastian, España: Springer. |
Files | Size | Format | View | Description |
---|---|---|---|---|
Formal Verification of Molecular ... | 292.2Kb | [PDF] | View/ | |