dc.creator | Lambán Pardo, Laureano | es |
dc.creator | Martín Mateos, Francisco Jesús | es |
dc.creator | Rubio, Julio | es |
dc.creator | Ruiz Reina, José Luis | es |
dc.date.accessioned | 2019-05-16T08:18:49Z | |
dc.date.available | 2019-05-16T08:18:49Z | |
dc.date.issued | 2017 | |
dc.identifier.citation | Lambán Pardo, L., Martín Mateos, F.J., Rubio, J. y Ruiz Reina, J.L. (2017). Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms. En ITP 2017: 8th International Conference on Interactive Theorem Proving (354-370), Brasília, Brazil: Springer. | |
dc.identifier.isbn | 978-3-319-66106-3 | es |
dc.identifier.issn | 0302-9743 | es |
dc.identifier.uri | https://hdl.handle.net/11441/86421 | |
dc.description.abstract | We present here an application of abstract single threaded
objects (abstract stobjs) in the ACL2 theorem prover, to define a formally
verified algorithm that given a matrix with elements in the ring
of integers, computes an equivalent matrix in column echelon form.
Abstract stobjs allow us to define a sound logical interface between matrices
defined as lists of lists, convenient for reasoning but inefficient, and
matrices represented as unidimensional stobjs arrays, which implement
accesses and (destructive) updates in constant time. Also, by means of
the abstract stobjs mechanism, we use a more convenient logical representation
of the transformation matrix, as a sequence of elemental transformations.
Although we describe here a particular normalization algorithm,
we think this approach could be useful to obtain formally verified
and efficient executable implementations of a number of matrix normal
form algorithms. | es |
dc.description.sponsorship | Ministerio de Ciencia e Innovación TIN2013-41086-P | es |
dc.description.sponsorship | Ministerio de Ciencia e Innovación MTM2014-54151-P | es |
dc.format | application/pdf | es |
dc.language.iso | eng | es |
dc.publisher | Springer | es |
dc.relation.ispartof | ITP 2017: 8th International Conference on Interactive Theorem Proving (2017), p 354-370 | |
dc.rights | Attribution-NonCommercial-NoDerivatives 4.0 Internacional | * |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | * |
dc.subject | Matrices | es |
dc.subject | ACL2 | es |
dc.subject | Abstract stobjs | es |
dc.subject | Matrix normal forms | es |
dc.title | Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms | es |
dc.type | info:eu-repo/semantics/conferenceObject | es |
dcterms.identifier | https://ror.org/03yxnpp24 | |
dc.type.version | info:eu-repo/semantics/submittedVersion | 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 | TIN2013-41086-P | es |
dc.relation.projectID | MTM2014-54151-P | es |
dc.relation.publisherversion | https://link.springer.com/chapter/10.1007/978-3-319-66107-0_23 | es |
dc.identifier.doi | 10.1007/978-3-319-66107-0_23 | es |
dc.contributor.group | Universidad de Sevilla. TIC137: Lógica, Computación e Ingeniería del Conocimiento | es |
idus.format.extent | 17 | es |
dc.publication.initialPage | 354 | es |
dc.publication.endPage | 370 | es |
dc.eventtitle | ITP 2017: 8th International Conference on Interactive Theorem Proving | es |
dc.eventinstitution | Brasília, Brazil | es |
dc.relation.publicationplace | Berlin | es |