Now showing items 1-6 of 6
Verification of the Formal Concept Analysis [Article]
(Real Academia de Ciencias, 2004)
This paper is concerned with a formal verification of the Formal Concept Analysis framework. We use the PVS system to represent and formally verify some algorithms of this theory. We also develop a method to transform ...
Formal Correctness of a Quadratic Unification Algorithm [Article]
We present a case study using ACL2  to verify a non-trivial algorithm that uses efficient data structures. The algorithm receives as input two first-order terms and it returns a most general unifier of these terms if ...
Constructing Formally Verified Reasoners for the ALC Description Logic [Article]
Description Logics are a family of logics used to represent and reason about conceptual and terminological knowledge. Recently, its importance has been increased since they are used as a basis for the Ontology Web Language ...
A Formal Proof of Dickson’s Lemma in ACL2 [Presentation]
Dickson’s Lemma is the main result needed to prove the termination of Buchberger’s algorithm for computing Gr¨obner basis of polynomial ideals. In this case study, we present a formal proof of Dickson’s Lemma using the ...
Formal verification of a generic framework to synthesize SAT-provers [Article]
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 ...
Formal proofs about rewriting using ACL2 [Article]
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 ...