Molecular Computation Models in ACL2: a Simulation of Lipton’s Experiment Solving SAT

Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Pérez Jiménez, Mario de Jesús; Sancho Caparrini, Fernando

Ponencia

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

Ficheros	Tamaño	Formato	Ver	Descripción
2002-ACL2-Adleman.pdf	195.1Kb	[PDF]	Ver/Abrir

Este registro aparece en las siguientes colecciones

Ponencias (Ciencias de la Computación e Inteligencia Artificial)

Mostrar el registro sencillo del ítem

Excepto si se señala otra cosa, la licencia del ítem se describe como: Attribution-NonCommercial-NoDerivatives 4.0 Internacional