- Bayesian learning and reasoning, 2000-2001, CONACYT-REDII
In this research we seek to develop Bayesian and reinforcement learning algorithms for multiagent systems. The area of application is user modeling
- Formal methods for hardware verification, 1998-1999, CONACYT-REDII
In this project we helped in the development of an interface between the HOL theorem prover (Higher-Order logic) and the CLAM proof planner.
HOL is a theorem prover developed by Mike Gordon and his group at Cambridge University. Clam is a proof planner developed by Alan Bundy
and his group at Edinburgh University. We worked with Richard Boulton, Edinburgh University in translating examples verified in the Clam-Oyster System
into the Clam-HOL System
- Proof Plans for Hardware Verification, 1994-1996 (CONACYT)
In this research we developed a proof engineering approach for automating the verification of circuits. We used the CLAM proof planner to guide the
Oyster proof checker in searching for a proof, given a conjecture. The conjecture is an implication where the antecedent is a formula describing a
circuit implementation and the consequent is another formula describing the specification of the circuit. The main heuristic used by CLAM is called "Rippling", which is used to automate mathematical induction.
- Expert systems in manufacturing 1990-1994 (CYDSA-CONACYT)
This was a program sponsored by CYDSA Corporation and by CONACYT to develop expert systems in manufacturing in CYDSA´s plants.
We developed around 20 intelligent system application during four years.
- AI Techniques in steel industry, 1990-1994 (HYLSA-CONACYT)
This was a program sponsored by HYLSA Corporation and by CONACYT to develop expert systems in manufacturing in some of HYLSA´s processes..
We developed around 4 intelligent system application during four years.
- Apple Computer University Consortium, 1986-1989, Apple Computer Latin America