| Department of Computer Science | Phone: (301) 405-2716 |
| University of Maryland | Fax: (301) 405-6707 |
| College Park, MD 20742 | e-mail: cruizc@cs.umd.edu |
| U. S. A. | URL= http://www.cs.umd.edu/~cruizc/ |
August 1996 (expected) Ph.D. in Computer Science.
1990 MS in Computer Science.
1989 BS in Mathematics.
1988 BS (5 year degree) in Computer Science.
I introduce and investigate formalisms that admit several forms of default negation which interact with each other and with classical (or ``explicit'') negation in the same knowledge based system. Some theoretical aspects of this research include the investigation of the expressive power of the new formalisms and the characterization of their semantics. Practical issues include implementing procedures to compute in these formalisms, calculating the computational complexity of different reasoning tasks under the proposed semantics and modeling real life applications. One example is the problem of merging several knowledge bases, each of which uses a different rule for negation, and finding answers to queries in the combined knowledge base.
For more details, see my doctoral dissertation description.
Categorical Logic. Showed that the category Dyn($\Sigma$) of automata and dynamorphisms over an alphabet $\Sigma$, and of the category MooreMch($\Sigma$) of Moore automata and Moore dynamorphisms over $\Sigma$ are presheaf topoi, and investigated their exponentials and subobject classifiers. Constructed free automata and free Moore automata over sets by respectively using the left adjoints of the forgetful functors from Dyn($\Sigma$) and MooreMch($\Sigma$) into the category of sets (which assign to each automaton or Moore automaton its set of states). Proved that each regular language over $\Sigma$ corresponds to the evaluation of the characteristic morphism associated with the inclusion of the empty subautomaton at the initial state of the accepting automaton.
Formal Verification of Abstract Data Types and Code Synthesis. Designed and developed an environment for the definition and manipulation of Abstract Data Types (ADTs), which provides a code synthesizer that automatically generates code in LISP and/or C which structurally and functionally implements an ADT. This code may be used in common applications. The environment includes also a theorem prover oriented to perform formal verification of ADTs as well as proving abstract properties of ADTs. It uses rewriting rules to produce and deal with canonical forms of ADT expressions.
Theorem Proving. Developed an implementation of the well-known theorem prover of R. Boyer and J.S. Moore characterized by allowing the definition of inductive objects and recursive functions, and using induction on well-founded orders as an essential part of theorem proving itself.
| - | Professor Jack Minker (Dissertation Advisor) | |
| Department of Computer Science University of Maryland College Park, MD 20742 U. S. A. |
e-mail: minker@cs.umd.edu Phone: (301) 405-2716 Fax: (301) 405-6707 | |
| - | Professor Michael Gelfond | |
| Department of Computer Science University of Texas at El Paso El Paso, TX 79968 U. S. A. |
e-mail: mgelfond@cs.utep.edu
Phone: (915) 747-6957 Fax: (915) 747-5030 | |
| - | Professor Donald Perlis | |
| Department of Computer Science University of Maryland College Park, MD 20742 U. S. A. |
e-mail: perlis@cs.umd.edu Phone: (301) 405-2685 Fax: (301) 405-6707 | |
| - | Professor V.S. Subrahmanian | |
| Department of Computer Science University of Maryland College Park, MD 20742 U. S. A. |
e-mail: vssecr@cs.umd.edu Phone: (301) 405-2711 Fax: (301) 405-6707 |