Artículos (Ciencias de la Computación e Inteligencia Artificial)https://hdl.handle.net/11441/113022019-05-19T19:06:08Z2019-05-19T19:06:08ZProof Pearl: a Formal Proof of Higman’s Lemma in ACL2https://hdl.handle.net/11441/862932019-05-13T11:32:30Z2011-01-01T00:00:00ZProof Pearl: a Formal Proof of Higman’s Lemma in ACL2
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. Our formalization
is based on a proof by Murthy and Russell, where the key termination argument
is justified by the multiset relation induced by a well-founded relation. To our
knowledge, this is the first mechanization of this proof.
2011-01-01T00:00:00ZFormalization of a normalization theorem in simplicial topologyhttps://hdl.handle.net/11441/862802019-05-13T09:53:47Z2012-01-01T00:00:00ZFormalization of a normalization theorem in simplicial topology
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, and a smaller
chain complex for the same simplicial set, called the normalized chain complex.
Even if the Normalization Theorem is usually stated as a higher-order result (with
a Category Theory flavor) we manage to give a first-order proof of it. To this aim
it is instrumental the introduction of an algebraic data structure called simplicial
polynomial. As a demonstration of the validity of our techniques we developed a
formal proof in the ACL2 theorem prover.
2012-01-01T00:00:00ZFormal verification of a generic framework to synthesize SAT-provershttps://hdl.handle.net/11441/862692019-05-10T09:26:51Z2004-01-01T00:00:00ZFormal verification of a generic framework to synthesize SAT-provers
We present in this paper an application of the ACL2 system to generate
and reason about propositional satis ability provers. For that purpose, we develop a
framework where we de ne a generic SAT-prover based on transformation rules, and
we formalize this generic framework in the ACL2 logic, carrying out a formal proof of
its termination, soundness and completeness. This generic framework can be
instantiated to obtain a number of veri ed and executable SAT-provers in ACL2, and
this can be done in an automated way. Three instantiations of the generic framework
are considered: semantic tableaux, sequent and Davis-Putnam-Logeman-Loveland
methods.
2004-01-01T00:00:00ZFormal proofs about rewriting using ACL2https://hdl.handle.net/11441/862662019-05-09T08:46:53Z2002-01-01T00:00:00ZFormal proofs about rewriting using ACL2
We present an application of the ACL2 theorem prover to reason about rewrite systems
theory. We describe the formalization and representation aspects of our work using the firstorder,
quantifier-free logic of ACL2 and we sketch some of the main points of the proof effort.
First, we present a formalization of abstract reduction systems and then we show how this
abstraction can be instantiated to establish results about term rewriting. The main theorems
we mechanically proved are Newman’s lemma (for abstract reductions) and Knuth–Bendix
critical pair theorem (for term rewriting).
2002-01-01T00:00:00Z