Buscar
Mostrando ítems 1-3 de 3
Ponencia
Formal Reasoning about Efficient Data Structures: A Case Study in ACL2
(Springer, 2003)
We describe in this paper the formal verification, using the ACL2 system, of a syntactic unification algorithm where terms are represented as directed acyclic graphs (dags) and these graphs are stored in a single-threaded ...
Ponencia
Formal Verification of Molecular Computational Models in ACL2: A Case Study
(Springer, 2003)
Theorem proving is a classical AI problem with a broad range of applications. Since its complexity is exponential in the size of the problem, many methods to parallelize the process has been proposed. One of these ...
Ponencia
A Formal Proof of Dickson’s Lemma in ACL2
(Springer, 2003)
Dickson’s Lemma is the main result needed to prove the termination of Buchberger’s algorithm for computing Gr¨obner basis of polynomial ideals. In this case study, we present a formal proof of Dickson’s Lemma using the ...