I just read you post. I agree with Ken, "A First course in Logic" is a good book. You have probably found it already, but you can read bits of the book on Amazon. I agree with Ken, it has the right style for easy reading/comprehension.
My company is building a Rule Engine/Inference Engine as well, and in my own research I have dived heavily into Russell and Godel.
I was visiting a friend in Canada about 4 weeks ago, and my friend said "Oh, you really want to read this book, 'Godel, Escher, Bach' (Douglas R Hofstadter)" and he bought if for me. It's 743 pages, and my copy is in tatters already. It's hard to put down.
If you want to know a great deal about formal logic from the ground up, inside and out and in very simple language, then GEB is probably the most amazing read you'll ever have on the subject. Just Google the title, and you'll see that I'm not alone in this thought, and if you've read any of my posts...I am quite the sceptic when I need to be. I thought it (GEB) would be crud...but it really is an amazing work and obviously written with great passion. It's hard not to get excited about the subject when you read what Hofstadter has to say.
I have an ORM model that I'm working on, and it's within a paper that I'm submitting for the conference. If it's accepted (the paper) you'll see it here. Either way I'll get a copy to you. I don't mind sharing it, because it is our precedent work so that nobody can say we didn't think of it first. Either way, be prepared for a head spin of significant proportion.
In essence, you can just use an ORM meta-model to do what you want to do, because FactTypes 'are' relations, and simple ORM models 'are' Theorems in FirstOrderLogic (see below on SOL). You could just use nORMa's meta schema, you just need to write your own interpretter.
Basically, Turin's 'Halting Problem', 'Isomorphism', 'Interpretation', and Godel's incompleteness theorems (outlined beautifully in GEB) are your major stumbling blocks. Once you have them/those concepts mastered, then you'll be able to nail a 'Rule Engine'/'Inference Engine'.
NB See pages 456 to 469 of Terry's new book for information about 'Interpretation'...basically, if you are building a RuleEngine, you have to watch out for Second/HigherOrderLogical 'interpretations' of Theorems. Dr Halpin and Dr Morgan suggest some ways to avoid problems there. They acknowledge an undocumented 'debate' as to the 'interpretation' of theorems of ORM (as either FOL or SOL in their 'interpretation'), and I agree it exists. I have my strategy for dealing with this, Dr Halpin is obviously looking for ways to deal with this, and (if you are asking....)..you'll come accross that one too. My position is that isomorphic interpretations of theorems of FOL as theorems of SOL/HOL are unavoidable altogether (e.g. my post in the Philosophy section), but I don't see a problem with that (it's all in the interpretation). i.e. Dr Halpin has to worry about 'everybodies' interpretation of an ORM model....you (on the other hand) as a developer of a Inference Engine get to chose when to 'stop' (Turin's 'Halting Problem') and whether you will 'ever' interpret S/HOL. i.e. you only have to deal with your own interpretters interpretation. There's still problems...but you don't have Halpin/Morgan's dilemma of having to deal with 'unknown' interpretters at design time....you just have to deal with 'unknown models at design time'...anyway, you'll see what I mean
Well, that's as much as I know.
I'll race you to the finish line ;) Who knows, we may share/compare notes.