Buscar
Mostrando ítems 1-10 de 28
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
Towards a Practical Argumentative Reasoning with Qualitative Spatial Databases
(Springer, 2003)
Classical database management can be flawed if the Knowledge database is built within a complex Knowledge Domain. We must then deal withinconsistencies and, in general, withanomalies of several types. In this paper we ...
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
Sistema certificado de decisión proposicional basado en polinomios
(Universidad de Sevilla, Departamento de Ciencias de la Computación e Inteligencia Artificial, 2009)
En [2] introducimos una regla de inferencia para la lógica proposicional (basado en el uso de la derivación de polinomios) denominada regla de independencia, diseñada para el cálculo de retracciones conservativas, y que ...
Ponencia
A Certified Polynomial-Based Decision Procedure for Propositional Logic
(Springer, 2001)
In this paper we present the formalization of a decision procedure for Propositional Logic based on polynomial normalization. This formalization is suitable for its automatic verification in an applicative logic like Acl2. ...
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)