My Current HOL Algorithm

The following is equivalent in strength to HOL Light. Continues this post.

• As an extension of the notion of term (defined here), add the notation of polymorphically typed lambda calculus, an equality predicate, and the choice operator (I'll call it epsilon-- it's a function that takes predicates and forms a term that represents an arbitrary satisfier of the predicate, if one exists; otherwise, it just represents an arbitrary term).
• Take terms with boolean type as a drop-in replacement for atomic statements in that design. (It may seem strange to use them to replace atomic statements, since they are compound statements, but bear with me. Rules will correspond to valid sequents, rather than to compound statements in the logic.)
• Use lambda-calculus unification as a drop-in replacement for first-order unification. This includes normalization; we could either store the normal forms of statements in the KB or let the unification algorithm normalize on the spot, depending on whether space efficiency of the KB or time efficiency of the unifier is a bigger concern.
• Implement equational reasoning. Fundamentally, we treat an equality statement which has a given truth value, T, as if it represented two rules with that truth value: one justifying inferences in each direction, substituting one term for another. These rules cannot be stated as FOL rules, however, since they represent substitution of terms within larger statements. Nonetheless, the same basic propagation scheme for the truth values will work. In addition to the 2 pseudo-rules for each equality statement, we treat the system as knowing A=A for all terms A. Knuth-Bendix completion should be implemented eventually, which allows us to ignore one of the two inference directions for each equality statement without losing anything. Ultimately, I believe this means equational reasoning can be implemented as an extension to the normalization step of the unification algorithm (but I could be wrong here).
• Finally, we also need one hypothetical reasoning rule: if assuming A implies B with truth calue TV1, and assuming B implies A with truth value TV2, then A=B with truth value (& TV1 TV2) for an appropriate &-formula. Rather than implementing this as one complicated hypothetical reasoning step, it seems to me that the most convenient way would be to implement rule-level reasoning in general (ie, a query can be a rule, rules can be combined with other rules to produce new rules, etc) and then add this as a way of recording high-probability mutual implication.

That's all, folks!

PS:

In addition to the above reasoning system, for HOL Light, we also need the axiom of choice and the axiom of infinity. (The axiom of extensionality is covered by normalization.) Both of these axioms are very much "mathematical" in nature, and it isn't clear whether they are needed for more common-sense reasoning. (My suspicion is that they would emerge in other forms, ie, in coding the KB we'd encode something like these plus much more.)

HOL update

YKY doesn't want to focus on HOL at the moment, but he suggested I write down my thoughts anyway. I was going to put it off since I'd really want to do a more detailed write-up taking care of all the loose ends, but since there is some interest from Russel, I'm outlining my approach now.

The approach is to translate system IG from the paper Illative Combinatory Logic. This is an untyped lambda-calculus logic which soundly & completely interprets first-order logic both "directly" (ie, as truth functions) and via curry-howard isomorphism (which indicates the strength of the type reasoning the system can interpret).

The way I'm planning on translating it is to treat a statement and its negation as essentially separate statements in the probability distribution; ie, the Liar sentence can have probability 0, but its negation can simultaneously have probability 0. Only when we know a statement is a proposition can we derive that P(prop) = 1 - P(~prop).

After this, what we do is just encode the valid sequents as rules in our existing logic. However, IG has an infinite number of valid sequents, specified with some sequent derivation rules. This means that we've got an infinite number of rules now-- we need an efficient mechanism for constructing valid rules as they are needed. The sequent derivation rules get turned into "meta-rules" in our logic. This is a bit complicated, but better than the alternatives (see my previous post).

One complication is that sequent-based need to be combined with something like the noisy-or combination rule [I need to add a reference...]. At present we're planning on dealing with this by having noisy-or be the default combination rule in the whole system; there are some cases where it is a terrible rule, though. YKY thinks we can determine which cases to apply it to using causal reasoning.

For efficient reasoning, we'd like to normalize terms before reasoning so that we can quickly recognize equality. However, in untyped HOL, some terms have nonterminating normalizations. There are a few things we can do. One is to just have a time cutoff on normalization attempts. Another is to try and do some type reasoning before normalization (so we'd only normalize when we could first prove termination). A third option that might have some interesting properties is what I'm calling "compressive normalization"... rather than the usual normalization, use the shortest form of a term as the normal form. This is non-terminating and we'd still need a time cutoff, but unlike the usual normal form, it exists even for terms which aren't propositions-- it just always exists. It might be useful to keep short forms of terms around for compression purposes.

Speaking of compression; integrating both HOL and likelihood reasoning into Gen means that might be feasible to specify a prior probability distribution over models within Gen itself, meaning iduction just becomes probabilistic deduction. However, I have not worked out details here.

That's all for today! :)