dc.creator | Martín Mateos, Francisco Jesús | es |
dc.creator | Alonso Jiménez, José Antonio | es |
dc.creator | Hidalgo Doblado, María José | es |
dc.creator | Ruiz Reina, José Luis | es |
dc.date.accessioned | 2019-05-17T09:18:53Z | |
dc.date.available | 2019-05-17T09:18:53Z | |
dc.date.issued | 2001 | |
dc.identifier.citation | Martín Mateos, F.J., Alonso Jiménez, J.A., Hidalgo Doblado, M.J. y Ruiz Reina, J.L. (2001). Verifying an Applicative ATP Using Multiset Relations. En EUROCAST 2001: 8th International Workshop on Computer Aided Systems Theory (612-626), Las Palmas de Gran Canaria, España: Springer. | |
dc.identifier.isbn | 978-3-540-42959-3 | es |
dc.identifier.issn | 0302-9743 | es |
dc.identifier.uri | https://hdl.handle.net/11441/86473 | |
dc.description.abstract | We present in this paper a formalization of multiset relations
in the ACL2 theorem prover [6], and we show how multisets can be used
to mechanically prove non-trivial termination properties. Every relation
on a set A induces a relation on finite multisets over A; it can be shown
that the multiset relation induced by a well-founded relation is also wellfounded
[3]. We have carried out a mechanical proof of this property in
the ACL2 logic. This allows us to provide well-founded multiset relations
in order to prove termination of recursive functions. Once termination is
proved, the function definition is admitted as an axiom in the logic and
formal mechanized reasoning about it is possible. As a major application
of this tool, we show how multisets can be used to prove termination of
a tableaux based theorem prover for propositional logic. | es |
dc.description.sponsorship | Ministerio de Ciencia y Tecnología TIC2000-1368-C03-02 | es |
dc.description.sponsorship | Ministerio de Ciencia y Tecnología PB96-1345 | es |
dc.format | application/pdf | es |
dc.language.iso | eng | es |
dc.publisher | Springer | es |
dc.relation.ispartof | EUROCAST 2001: 8th International Workshop on Computer Aided Systems Theory (2001), p 612-626 | |
dc.rights | Attribution-NonCommercial-NoDerivatives 4.0 Internacional | * |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | * |
dc.title | Verifying an Applicative ATP Using Multiset Relations | 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 | TIC2000-1368-C03-02 | es |
dc.relation.projectID | PB96-1345 | es |
dc.relation.publisherversion | https://link.springer.com/chapter/10.1007/3-540-45654-6_47 | es |
dc.identifier.doi | 10.1007/3-540-45654-6_47 | es |
dc.contributor.group | Universidad de Sevilla. TIC137: Lógica, Computación e Ingeniería del Conocimiento | es |
idus.format.extent | 15 | es |
dc.publication.initialPage | 612 | es |
dc.publication.endPage | 626 | es |
dc.eventtitle | EUROCAST 2001: 8th International Workshop on Computer Aided Systems Theory | es |
dc.eventinstitution | Las Palmas de Gran Canaria, España | es |
dc.relation.publicationplace | Berlin | es |
dc.identifier.sisius | 6523948 | es |