Ponencia
Verifying an Applicative ATP Using Multiset Relations
Autor/es | Martín Mateos, Francisco Jesús
Alonso Jiménez, José Antonio Hidalgo Doblado, María José Ruiz Reina, José Luis |
Departamento | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial |
Fecha de publicación | 2001 |
Fecha de depósito | 2019-05-17 |
Publicado en |
|
ISBN/ISSN | 978-3-540-42959-3 0302-9743 |
Resumen | 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 ... 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. |
Identificador del proyecto | TIC2000-1368-C03-02
PB96-1345 |
Cita | 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. |
Ficheros | Tamaño | Formato | Ver | Descripción |
---|---|---|---|---|
Verifying an Applicative ATP.pdf | 272.0Kb | [PDF] | Ver/ | |