Buscar
Mostrando ítems 1-9 de 9
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
Formal proofs about rewriting using ACL2
(Springer, 2002)
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 ...
Artículo
Foundational Challenges in Automated Data and Ontology Cleaning in the Semantic Web
(IEEE Computer Society, 2006)
The application of automated reasoning systems to data cleaning in the Semantic Web raises many challenges on the foundational basis of cleaning agent design. The authors discuss some of them. They finally argue that ...
Artículo
Verification of the Formal Concept Analysis
(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 ...
Artículo
Constructing Formally Verified Reasoners for the ALC Description Logic
(Elsevier, 2008)
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 ...
Artículo
Formal Correctness of a Quadratic Unification Algorithm
(Springer, 2006)
We present a case study using ACL2 [5] 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 ...
Artículo
Formal verification of a generic framework to synthesize SAT-provers
(Springer, 2004)
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 ...
Ponencia
A Formal Proof of Dickson’s Lemma in ACL2
(Springer, 2003)
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 ...