dc.creator | Martín Mateos, Francisco Jesús | es |
dc.creator | Alonso Jiménez, José Antonio | es |
dc.creator | Pérez Jiménez, Mario de Jesús | es |
dc.creator | Sancho Caparrini, Fernando | es |
dc.date.accessioned | 2016-09-13T09:20:18Z | |
dc.date.available | 2016-09-13T09:20:18Z | |
dc.date.issued | 2002 | |
dc.identifier.citation | Martín Mateos, F.J., Alonso Jiménez, J.A., Pérez Jiménez, M.d.J. y Sancho Caparrini, F. (2002). Molecular Computation Models in ACL2: a Simulation of Lipton’s Experiment Solving SAT. Recuperado de | |
dc.identifier.uri | http://hdl.handle.net/11441/44936 | |
dc.description.abstract | In this paper we present an ACL2 formalization of a molecular computing model: Adleman’s
restricted model [2]. This is a first step to formalize unconventional models of computation
in ACL2. As an application of this model, an implementation of Lipton’s experiment
solving SAT [7] is described, based on the formalization given in [6]. We use ACL2 to make a
formal proof of the completeness and soundness properties of the function implementing the
experiment | es |
dc.description.sponsorship | Ministerio de Ciencia y Tecnología TIC2000-1368-CO3-02 | es |
dc.format | application/pdf | es |
dc.language.iso | eng | es |
dc.relation.ispartof | Third International Workshop on the ACL2 Theorem Prover and Its Applications (2002), p 175-187 | |
dc.rights | Attribution-NonCommercial-NoDerivatives 4.0 Internacional | * |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | * |
dc.title | Molecular Computation Models in ACL2: a Simulation of Lipton’s Experiment Solving SAT | es |
dc.type | info:eu-repo/semantics/conferenceObject | es |
dcterms.identifier | https://ror.org/03yxnpp24 | |
dc.type.version | info:eu-repo/semantics/publishedVersion | es |
dc.rights.accessRights | info:eu-repo/semantics/openAccess | es |
dc.contributor.affiliation | Universidad de sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial | es |
dc.relation.projectID | TIC2000-1368-CO3-02 | es |
idus.format.extent | 13 | es |
dc.publication.initialPage | 175 | es |
dc.publication.endPage | 187 | es |
dc.eventtitle | Third International Workshop on the ACL2 Theorem Prover and Its Applications | es |
dc.eventinstitution | Grenoble | es |
dc.relation.publicationplace | Grenoble | es |
dc.identifier.idus | https://idus.us.es/xmlui/handle/11441/44936 | |
dc.contributor.funder | Ministerio de Ciencia y Tecnología (MCYT). España | |