Buscar
Mostrando ítems 1-5 de 5
Artículo
Verifying the bridge between simplicial topology and algebra: the Eilenberg–Zilber algorithm
(Oxford Academic, 2013)
The Eilenberg–Zilber algorithm is one of the central components of the computer algebra system called Kenzo, devoted to computing in Algebraic Topology. In this article we report on a complete formal proof of the underlying ...
Artículo
Formally Verified Tableau-Based Reasoners for a Description Logic
(Springer, 2014)
Description Logics are a family of logics used to represent and reason about conceptual and terminological knowledge. One of the most basic description logics is ALC , used as a basis from which to obtain others. Description ...
Artículo
Proof Pearl: a Formal Proof of Higman’s Lemma in ACL2
(Springer, 2011)
Higman’s lemma is an important result in infinitary combinatorics, which has been formalized in several theorem provers. In this paper we present a formalization and proof of Higman’s Lemma in the ACL2 theorem prover. ...
Artículo
Formalization of a normalization theorem in simplicial topology
(Springer, 2012)
In this paper we present a complete formalization of the Normalization Theorem, a result in Algebraic Simplicial Topology stating that there exists a homotopy equivalence between the chain complex of a simplicial set, ...
Artículo
A verified Common Lisp implementation of Buchberger's algorithm in ACL2
(Elsevier, 2010)
In this article, we present the formal verification of a Common Lisp implementation of Buchberger's algorithm for computing Gröbner bases of polynomial ideals. This work is carried out in ACL2, a system which provides ...