Buscar
Mostrando ítems 1-10 de 17
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
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 ...
Artículo
Formal proofs about rewriting using ACL2
(Springer, 2002)
We present an application of the ACL2 theorem prover to reason about rewrite systems theory. We describe the formalization and representation aspects of our work using the firstorder, quantifier-free logic of ACL2 and ...
Ponencia
Multiset Relations: A Tool for Proving Termination
(University of Texas, 2000)
Ponencia
Formalizing Rewriting in the ACL2 Theorem Prover
(Springer, 2000)
We present an application of the ACL2 theorem prover to formalize and reason about rewrite systems theory. This can be seen as a first approach to apply formal methods, using ACL2, to the design of symbolic computation ...
Ponencia
Verification in ACL2 of a Generic Framework to Synthesize SAT–Provers
(Springer, 2002)
We present in this paper an application of the ACL2 system to reason about propositional satisfiability provers. For that purpose, we present a framework where we define a generic transformation based SAT–prover, and ...
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 ...
Artículo
Verification of the Formal Concept Analysis
(Real Academia de Ciencias, 2004)
This paper is concerned with a formal verification of the Formal Concept Analysis framework. We use the PVS system to represent and formally verify some algorithms of this theory. We also develop a method to transform ...
Artículo
Constructing Formally Verified Reasoners for the ALC Description Logic
(Elsevier, 2008)
Description Logics are a family of logics used to represent and reason about conceptual and terminological knowledge. Recently, its importance has been increased since they are used as a basis for the Ontology Web Language ...