MadMode

Prompted by a question about RDF schemas for dollars, gallons, and other units, I found myself looking into SUMO again.

The SUMO/wordnet mappings are great, and the SUMO time concepts are backed by a nice KIF formalization of Allen's work, but it's overly constrained; I prefer the cyc style where the before and after relations apply to conferences and events, without indirection via time intervals.

But what got me really thinking was the way holdsDuring takes formulas as arguments, despite the claim that SUMO is written in SUO-KIF, which has pretty traditional first-order syntax and semantics. I eventually found this addressed explicitly:

... SUMO does include a number of predicates that take formulae as arguments, such as holdsDuring, believes, and KappaFn. In Sigma, we also perform a number of "tricks" which allow the user to state things which appears to be higher order, but which are in fact first order and have a simple syntactic transformation to standard first order form.

How does SUMO employ higher order logic? in the Ontology Portal FAQ, March 2005

I'm curious about how variables are handled in these tricks. The code is all there, and I downloaded it, but I didn't get very far.

I actually don't think first-order semantics are the best fit for the Semantic Web, where formulas refer to documents and the formulas they contain; reflection is a key mechanism, and prohibiting loops is unscalable. I think constructive proof is a much better way to think about proofs in N3.

I discovered Artemov's explicit provability stuff a while ago; my notes date from September 2003:

... explicit provability provides a tool of increasing the efficiency of a formal system by verified rules without explosion of the metamathematical level of the system.

So I dug out my LogicOfProofs larch transcription notes and the Explicit provability and constructive semantics article from the Bulletin of Symbolic Logic, volume 7, No.1, pp. 1-36, 2001 and started working on lp.n3, and an N3 rule for the constructive form of modus ponens:

# application
{ (t s) comp ts.
  t proves { F => G }.
  s proves F
 }
  => {  ts proves G }.

that is: if t is an algorithm for proving that F implies G, and s is an algorithm for proving s, then the composition of s and t is an algorithm for proving G. This Curry-Howard correspondence is really nifty.

The proof that "Socrates is mortal" from "if Socrates is a man then he is mortal" and "Socrates is a man" looks like:

2000/10/swap$ python cwm.py util/lp.n3 --think
...
      ( lpex:a2
        lpex:a1 )
         a l:_g0;
         :comp  [
             a :Proof;
             :proves {lpex:Socrates     a lpex:Mortal .
            } ] .

    lpex:a1     a :Proof;
         :proves {lpex:Socrates     a lpex:Man .
        } .

    lpex:a2     a :Proof;
         :proves {{
            lpex:Socrates     a lpex:Man .

            }     log:implies {lpex:Socrates     a lpex:Mortal .
            } .
        } .

... which is much easier to read than cwm's --why style:

2000/10/swap$ python cwm.py test/reason/socrates.n3 --think --why
     @forSome :_g0 .
      [      a pr:Conjunction,
                    pr:Proof;
             pr:component  [
                 a pr:Inference;
                 pr:evidence  (
                 [
                         a pr:Extraction;
                         pr:because :_g0;
                         pr:gives {:socrates     a :Man .
                        } ] );
                 pr:rule  [
                     a pr:Extraction;
                     pr:because :_g0;
                     pr:gives {{
                        :socrates     a :Man .

                        }     log:implies {:socrates     a :Mortal .
                        } .
                    } ] ],
                    :_g0;
             pr:gives {:socrates     a :Man,
                        :Mortal .
            {
                :socrates     a :Man .

                }     log:implies {:socrates     a :Mortal .
                } .
            } ].

I didn't actually see formulas occuring as terms in that 2001 paper. So it might be a distraction with respect to the original holdsDuring issue. And that version of the logic of proofs includes all of propositional calculus, including the law of the excluded middle. But among his accomplishments I see

Reflexive lambda-calculus. The Curry-Howard isomorphism converting intuitionistic proofs into typed lambda-terms is a simple instance of an internalization property of a our system lambda-infinity which unifies intuitionistic propositions (types) with lambda-calculus and which is capable of internalizing its own derivations as lambda-terms.

so perhaps I should keep studying his stuff. I wish he'd use s-expressions and QUOTE like Moore's ACL2 paper and Chaitin's work rather than doing reflection with Godel numbering. I wonder what HA is; ah... wikipedia to the rescue:

It is essentially Peano arithmetic, minus the law of the excluded middle...