Buscar
Mostrando ítems 1-10 de 15
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
Molecular Computation Models in ACL2: a Simulation of Lipton’s Experiment Solving SAT
(2002)
In this paper we present an ACL2 formalization of a molecular computing model: Adleman’s restricted model [2]. This is a first step to formalize unconventional models of computation in ACL2. As an application of this ...
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
Expert System to Real Time Control of Machining Processes
(Springer, 2009)
Industrial machining processes use automated milling machines. These machines are connected to a control device that provides the basic instructions used to obtain a piece. However, these processes depend on the human ...
Ponencia
KRRT: Knowledge Representation and Reasoning Tutor System
(Springer, 2007)
Knowledge Representation & Reasoning (KR&R) is a fundamental topic in Artificial Intelligence. A basic KR language is First– Order Logic (FOL), the most representative logic–based representation language, which is part ...
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
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 ...