So I don’t remember a lot having to do with the logic engine, but I remember it being a difficult project. You see, I want to make something a little more interesting than a typical constraint solver. For this reason, it is supposed to be designed to simulate mathematical proof.
The simplest way to do this, is through the idea of inference. You take a given ‘state’, which could either be considered one statement or multiple logical statements (They are both equivalent in truth— two statements, say Q, P being true is identical to “Q ∧ P”)
And this is perfectly easy to do for simple propositional logic, like with DeMorgan’s laws and whatnot, but when you get into first-order and second-order, those quantifiers introduce some complexities.
For instance, what inference rule is seen in this proof?:
- A. All men are mortal [ ∀(x)(Hx → Mx) ]
- A. Socrates is a man [ Hs ]
- ∴ Socrates is mortal [ Ms ] Whereas other rules, like (Q ∨ P) ∧ ¬Q ∴ P can be easily searched for, this one, which may considered thusly: ∀(x)(y) ∧ ANYTHING → y{With whatever “x” is in y, being replaced with ‘ANYTHING’}
(This is oversimplified, but it demonstrates the basic problem).
In order to simulate the first, simpler kinds of rules, a procedure must be created to
- Detect whether a given statement matches the form of such a rule
- Categorize which parts of the statement belong to which parts of the rule
- Replace those parts of the conclusion which are also in the rule, with the matching parts of the statement This is very close to the same procedure you’d need for universal statements. Converting such universal statements in the form [ ∀(x)(x → y) ] to the rule [ x ∴ y ] is extremely simple.
Another option is to make a rule, every time that a universal statement is introduced, that is of the form, given a universal statement ∀(x)(p), would be [ x ∴ p ]. I haven’t noticed a problem with this line of thought yet.