
.
Grants
Grant holder:
 Bayesian learning and reasoning, 20002001, CONACYTREDII
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, 19981999, CONACYTREDII
In this project we helped in the development of an interface between the HOL theorem prover (HigherOrder 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 ClamOyster System
into the ClamHOL System
 Proof Plans for Hardware Verification, 19941996 (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 19901994 (CYDSACONACYT)
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, 19901994 (HYLSACONACYT)
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.
Grant manager:
 Apple Computer University Consortium, 19861989, Apple Computer Latin America


