Buscar
Mostrando ítems 11-15 de 15
Ponencia
ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System
(Springer, 2009)
Kenzo is a Computer Algebra system devoted to Algebraic Topology, and written in the Common Lisp programming language. It is a descendant of a previous system called EAT (for Effective Algebraic Topology). Kenzo shows ...
Ponencia
Rete Algorithm Applied to Robotic Soccer
(Springer, 2005)
This article is a first approach to the use of Rete algorithm to design a team of robotic soccer playing agents for Robocup Soccer Server. Rete algorithm is widely used to design rule-based expert systems. Robocup Soccer ...
Ponencia
Formal Verification of Molecular Computational Models in ACL2: A Case Study
(Springer, 2003)
Theorem proving is a classical AI problem with a broad range of applications. Since its complexity is exponential in the size of the problem, many methods to parallelize the process has been proposed. One of these ...
Ponencia
Verifying an Applicative ATP Using Multiset Relations
(Springer, 2001)
We present in this paper a formalization of multiset relations in the ACL2 theorem prover [6], and we show how multisets can be used to mechanically prove non-trivial termination properties. Every relation on a set A ...
Ponencia
A Formally Verified Prover for the ALC Description Logic
(Springer, 2007)
The Ontology Web Language (OWL) is a language used for the Semantic Web. OWL is based on Description Logics (DLs), a family of logical formalisms for representing and reasoning about conceptual and terminological ...