Buscar
Mostrando ítems 1-4 de 4
Ponencia
A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory.
(University of Texas, 2002)
In some cases, when we develop a formal theory in ACL2, it would be desirable that the definitions and theorems of the theory be as independent of a concrete implementation as possible. This is particularly interesting ...
Ponencia
Progress Report: Term Dags Using Stobjs
(University of Texas, 2002)
We explore in this paper the use of efficient data structures to implement operations on first-order terms, that can be formally verified. Specifically, we present the status of our work on defining and verifying a ...
Ponencia
Towards a tool for ontology engineering
(IEEE Computer Society, 2004)
A tool based on a spatial representation of provisional ontologies is designed. The tool allows the cleming of Knowledge Bases, aa well to induce new concepts in early steps of the building of an ontology.
Ponencia
A Theory About First-Order Terms in ACL2
(University of Texas, 2002)
We describe the development in ACL2 of a library of results about first-order terms. In particular, we present the formalization of some of the main properties of the complete lattice of first-order terms with respect ...