[FOM] models for logic and model checking

[shane]

Hi,

I am a senior level undergrad math major. I am taking a number
of I/S in mathematical logic from the chair [VCU], who has been
gracious enough to give me his time despite his heavy schedule.

I am writing, mostly for fun, a program that has a lex/parser for
some first order language. Right now all I have to do it take any
valid FOL formula (as verified by the grammer) and make it 
prenex. But going forward I want to turn it into a theorem prover
(probably dirt simple given my level of know-how).  And if that
is successful, add model checking capabilities.

In reading the literature -- especially SRI's Maude and Gries'
book on logic -- equational logic appears to be an ideal way
to model a general logic system that can have (most) any user 
defined theory, operators etc: it supports concurrency and the 
model admits both a logical and compuational point of view that 
(it has been argued) that does not come at the cost of efficiency.

But in actual fact, the number of possible choices seems absolutely 
endless especially by the time "temporal logic", HOL are added 
to the mix. Is there some paper I can read which gives me a lay-of-
the-land? I would like to know the trade offs so that once I try my
hand at first order logic I could plan for a more general model to
do theorem proving AND model checking within the same system.
I do know BDD seem to be an integral part of model checking but
barely more than that.

Also, I am aiming to go into a math Ph.d program (if they'll have me!!).
The universities in my area are U. of Virginia, John Hopkins, and
UMD Collegepark. If there's any recent or current graduate students
out there at these schools, please email me directly as I have a couple
of 
general/fact-finding questions to ask.

Regards,
Shane Miller
gshanemiller at comcast.net