First-order (predicate) logic for F#

Consider this problem from the Stanford Introduction to Logic course:

We know that horses are faster than dogs and that there is a greyhound that is faster than every rabbit. We know that Harry is a horse and that Ralph is a rabbit. Our job is to derive the fact that Harry is faster than Ralph.

We write the premises (including implicit ones) in first-order logic as follows:

We can code this directly into F# using the Flogic DSL. For example, this says every greyhound is a dog:

ForAll (
    Variable "y",
    Implication (
        Formula (
            Predicate ("greyhound", 1),
            [| Term (Variable "y") |]),
        Formula (
            Predicate ("dog", 1),
            [| Term (Variable "y") |])))

However, rather than write out each premise the long way, we can use a parser instead:

let parser = Parser.makeParser ["harry"; "ralph"]      // tell the parser that harry and ralph are named constants
let premise = Parser.run parser "∀y.(g(y) ⇒ d(y))"    // every greyhound is a dog

We can then use the resolution principle to prove our goal:

let goal = Parser.run parser "f(harry, ralph)"
let proofOpt = LinearResolution.tryProve premises goal

This works by negating the goal and deriving a contradiction. In this case, proofOpt will hold the following steps: