Buscar
Mostrando ítems 1-9 de 9
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
A methodology for the computer-aided cleaning of complex knowledge databases
(IEEE Computer Society, 2002)
In environments with complex cognitive structure (such as semantic web or sophisticated spatial databases for geographical information systems), classical methods for detecting anomalies can be inadequate. In this paper ...
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
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 ...
Ponencia
ILP Operators for Propositional Connectionist Networks
(Wright State University, 2002)
Ponencia
A Quasi-Metric for Machine Learning
(Springer, 2002)
The subsumption relation is crucial in the Machine Learning systems based on a clausal representation. In this paper we present a class of operators for Machine Learning based on clauses which is a characterization of the ...