The shortest path problem is an important problem in graph theory, consisting in finding paths between two nodes in weighted ...

Steganography is the art of hiding the fact that comunication is taking place. In this project we present an introduction ...

A Decision Tree is a supervised learning technique used for prediction tasks, which stands out for being able to produce ...

QR codes are the most common way of storing and exchanging information. In this project they will be studied in order to create a Haskell package with necessary functions and data types to implement them.

Artificial Neural Networks are a computational model whose objective is to simulate the learning system of the human brain, ...

In this project we establish the basic theoretical concepts about F inite State M achines and Model Checking so we can ...

We present here an application of abstract single threaded objects (abstract stobjs) in the ACL2 theorem prover, to define ...

In this paper, we present how algebraic structures and morphisms can be modelled in the ACL2 theorem prover. Namely, we ...

Description Logics are a family of logics used to represent and reason about conceptual and terminological knowledge. One ...

The Eilenberg–Zilber algorithm is one of the central components of the computer algebra system called Kenzo, devoted ...

Certified symbolic manipulation is an emerging new field where programs are accompanied by certificates that, suitably ...

El objetivo del trabajo es formalizar razonamiento complejo de forma legible por los humanos y procesable por las máquinas. ...

In this paper we present a complete formalization of the Normalization Theorem, a result in Algebraic Simplicial Topology ...

Higman’s lemma is an important result in infinitary combinatorics, which has been formalized in several theorem provers. ...

In this paper we present a complete formalization, using the ACL2 theorem prover, of the Normalization Theorem, a result ...

Aunque el proceso de fabricación por arranque de viruta ha evolucionado mucho en los últimos años con la incorporación de ...

Industrial machining processes use automated milling machines. These machines are connected to a control device that ...

Kenzo is a Computer Algebra system devoted to Algebraic Topology, and written in the Common Lisp programming language. It ...

Description Logics are a family of logics used to represent and reason about conceptual and terminological knowledge. ...

Knowledge Representation & Reasoning (KR&R) is a fundamental topic in Artificial Intelligence. A basic KR language is ...

The Ontology Web Language (OWL) is a language used for the Semantic Web. OWL is based on Description Logics (DLs), a ...

The application of automated reasoning systems to data cleaning in the Semantic Web raises many challenges on the foundational ...

We present a case study using ACL2 [5] to verify a non-trivial algorithm that uses efficient data structures. The algorithm ...

This article is a first approach to the use of Rete algorithm to design a team of robotic soccer playing agents for Robocup ...

This paper is concerned with a formal verification of the Formal Concept Analysis framework. We use the PVS system to ...

We present in this paper an application of the ACL2 system to generate and reason about propositional satis ability provers. ...

We describe in this paper the formal verification, using the ACL2 system, of a syntactic unification algorithm where terms ...

Theorem proving is a classical AI problem with a broad range of applications. Since its complexity is exponential in the ...

Dickson’s Lemma is the main result needed to prove the termination of Buchberger’s algorithm for computing Gr¨obner basis ...

In some cases, when we develop a formal theory in ACL2, it would be desirable that the definitions and theorems of the ...

In this paper we present an ACL2 formalization of a molecular computing model: Adleman’s restricted model [2]. This is a ...

We explore in this paper the use of efficient data structures to implement operations on first-order terms, that can be ...

We present an application of the ACL2 theorem prover to reason about rewrite systems theory. We describe the formalization ...

We present in this paper an application of the ACL2 system to reason about propositional satisfiability provers. For that ...

We describe the development in ACL2 of a library of results about first-order terms. In particular, we present the ...

The aim ofthis paper is to develop an executable prototype ofan unconventional model ofcomputation. Using the PVS ...

En este trabajo se desarrolla una formalización de sistemas de razonamiento proposicionales y se verifican automáticamente sus principales propiedades en el sistema de demostración automática ACL2.

We present in this paper a formalization of multiset relations in the ACL2 theorem prover [6], and we show how multisets ...

We present an application of the ACL2 theorem prover to formalize and reason about rewrite systems theory. This can be ...