rules

Building accountability appliances involves a challenging intersection between business, law, and technology. In my first blog about how to satisfy the legal portion of the triad, I explained that - conceptually - the lawyer would want to know whether particular digital transactions had complied with one or more rules. Lawyers, used to having things their own way, want more... they want to get the answer to that question in a particular structure.

All legal cases are decided using the same structure. As first year law students, we spend a year with highlighter in hand, trying to pick out the pieces of that structure from within the torrent of words of court decisions. Over time, we become proficient and -- like the child who stops moving his lips when he reads -- the activity becomes internalized and instinctive. From then on, we only notice that something's not right by its absence.

The structure is as follows:

• ISSUE - the legal question that is being answered. Most typically it begins with the word "whether" "Whether the Privacy Act was violated?" Though the bigger question is whether an entire law was violated, because laws tend to have so many subparts and variables, we often frame a much narrower issue based upon a subpart that we think was violated, such as "Whether the computer matching prohibition of the Privacy Act was violated?"

• RULE - provides the words and the source of the legal requirement. This can be the statement of a particular law, such as "The US Copyright law permits unauthorized use of copyrighted work based upon four conditions - the nature of use, the the nature of the work, the amount of the work used, and the likely impact on the value of the work. 17 USC § 107." Or, it can be a rule created by a court to explain how the law is implemented in practical situations: "In our jurisdiction, there is no infringement of a copyrighted work when the original is distributed widely for free because there is no diminution of market value. Field v. Google, Inc., 412 F. Supp 2d. 1106 (D.Nev. 2006)." [Note: The explanation of the citation formats for the sources has filled books and blogs. Here's a good brief explanation from Cornell.]

• FACTS - the known or asserted facts that are relevant to the rule we are considering and the source of the information. In a Privacy Act computer matching case, there will be assertions like "the defendant's CIO admitted in deposition that he matched the deadbeat dads list against the welfare list and if there were matches he was to divert the benefits to the custodial parent." In a copyright case fair use case, a statement of facts might include "plaintiff admitted that he has posted the material on his website and has no limitations on access or copying the work."
  

• ANALYSIS - is where the facts are pattern-matched to the rule. "The rule does not permit US persons to lose benefits based upon computer matched data unless certain conditions are met. Our facts show that many people lost their welfare benefits after the deadbeat data was matched to the welfare rolls without any of the other conditions being met." Or "There can be no finding of copyright infringement where the original work was so widely distributed for free that it had no market value. Our facts show that Twinky Co. posted its original material on the web on its own site and every other site where it could gain access without any attempt to control copying or access."


• CONCLUSION - whether a violation has or has not occurred. "The computer matching provision of the Privacy Act was violated." or "The copyright was not infringed.

In light of this structure, we've been working on parsing the tremendous volume of words into their bare essentials so that they can be stored and computed to determine whether certain uses of data occurred in compliance with law. Most of our examples have focused on privacy.

Today, the number of sub-rules, elements of rules, and facts are often so voluminous that there is not enough time for a lawyer or team of lawyers to work through them all. So, the lawyer guesses what's likely to be a problem and works from there; the more experienced or talented the lawyer, the more likely that the guess leads to a productive result. Conversely, this likely means that many violations are never discovered. One of the great benefits of our proposed accountability appliance is that it could quickly reason over a massive volume of sub-rules, elements, and facts to identify the transactiions that appear to violate a rule or for which there's insufficient information to make a determination.

Although we haven't discussed it, I think there also will be a benefit to be derived from all of the reasoning that concludes that activities were compliant. I'm going to try to think of some high value examples.

Two additional blogs are coming:

Physically, what does the lawyer expect to see? At the simplest level, lawyers are expecting to see things in terms they recognize and without unfamiliar distractions; even the presence of things like curly brackets or metatags will cause most to insist that the output is unreadable. Because there is so much information, visualization tools present opportunities for presentations that will be intuitively understood.

And:

The 1st Lawyer to Programmer/Programmer to Lawyer Dictionary! Compliance, auditing, privacy, and a host of other topics now have lawyers and system developers interacting regularly. As we've worked on DIG, I've noticed how the same words (e.g., rules, binding, fact) have different meanings.

I have a new bookmark. No, not a del.icio.us bookmark; not some bits in a file. This is the kind you have to go there to get.. go to Cleveland, that is. It reads:

Thank you
for you love & support
for the Ikpia & Ogbuji families
At this time of real need.
We will never forget
Imose, Chica, & Anya

Abundant Life International Church
Highland heights, OH

After working with Chime for a year or so on the GRDDL Working Group (he was the difference between a hodge-podge of test files and a nicely organized GRDDL Test Cases technical report), I was really excited to meet him at the W3C Technical Plenary in Cambridge in early November. His Fuxi work is one of the best implementations of the way I think semantic web rules and proofs should go. When he told me some people didn't see the practical applications, it made me want to fly there and tell them how I think this will save lives and end world hunger.

So this past Tuesday, when I read the news about his family, the only way I could make my peace with it was to go and be with him. I can only imagine what he is going through. Eric Miller and Brian and David drove me to the funeral, but the line to say hi to the family was too long. And the internment service didn't really provide an opportunity to talk. So I was really glad that after I filled my plate at the reception, a seat across from Chime and Roschelle opened up for me and I got to sit and share a meal with them.

Grandpa Linus was at the table, too. His eulogy earlier at the funeral ended with the most inspiring spoken rendition of a song that I have ever heard:

Now The Hacienda's Dark The Town Is Sleeping
Now The Time Has Come To Part The Time For Weeping
Vaya Con Dios My Darling
Vaya Con Dios My Love

His eulogy is also posted as Grandparents' lament on The Kingdom Kids web site, along with details about a fund to help the family get back on their feet.

We're long overdue for standard URIs for units of measure in the Semantic Web.

The SUMO stuff has a nice browser (e.g. see meter), a nice mapping from wordnet, and nice licensing terms. Of course, it's not RDF-native. In particular, it uses n-ary relations in the form of functions of more than one argument; 1 hour is written (&%MeasureFn 1 &%HourDuration). I might be willing to work out a mapping for that, but other details in the KIF source bother me a bit: a month is modelled conservatively as something between 28 and 31 days, but a year is exactly 365 days, despite leap-years. Go figure.

There's a nice Units in MathML note from November 2003, but all the URIs are incomplete, e.g. http://.../units/yard .

The Sep 2006 OWL Time Working Draft has full URIs such as http://www.w3.org/2006/time#seconds, but its approach to n-ary relations is unsound, as I pointed out in a Jun 2006 comment.

Tim sketched the Interpretation Properties idiom back in 1998; I don't suppose it fits in OWL-DL, but it appeals to me quite a bit as an approach to units of measure. He just recently fleshed out some details in http://www.w3.org/2007/ont/unit. Units of measure are modelled as properties that relate quantities to magnitudes; for example:

 track length [ un:mile 0.25].

This Interpretation Properties approach allows us to model composition of units in the natural way:

W is o2:chain of (A V).

where o2:chain is like property chaining in OWL 1.1 (we hope).

Likewise, inverse units are modelled as inverse properties:

s a Unit; rdfs:label "s".
hz rdfs:label "Hz"; owl:inverseOf s. 

Finally, scalar conversions are modelled using product; for example, mile is defined in terms of meter like so:

(m 0.0254) product inch.
(inch 12) product foot.
(foot 3) product yard.
(yard 22) product chain.
(chain 10) product furlong.
(furlong 8)product mile.

I supplemented his ontology with some test/example cases, unit_ex.n3 and then added a few rules to flesh out the modelling. These rules converts between meters and miles:

# numeric multiplication associates with unit multiplication
{ (?U1 ?S1) un:product ?U2.
  (?U2 ?S2) un:product ?U3.
  (?S1 ?S2) math:product ?S3
} => { (?U1 ?S3) un:product ?U3 }

# scalar conversions between units
{ ?X ?UNIT ?V.
  (?BASE ?CONVERSION) un:product ?UNIT.
  (?V ?CONVERSION) math:product ?V2.
} => { ?X ?BASE ?V2 }.

Put them together and out comes:

    ex:track     ex:length  [
             :chain 20.0;
             :foot 1320.0;
             :furlong 2.0;
             :inch 15840.0;
             :m 402.336;
             :mile 0.25;
             :yard 440.0 ] .

The rules I wrote for pushing conversion factors into chains isn't fully general, but it works in cases like converting from this:

(un:foot un:hz) o2:chain fps.
bullet speed [ fps 4000 ].

to this:

    ex:bullet     ex:speed  [
             ex:fps 4000;
             :mps 1219.2 ] .

As I say, I find this approach quite appealing. I hope to discuss it with people working on units of measure in development of a Delivery Context Ontology.

One my trip to Duke, just after I arrived on Thursday, Pat Hayes gave a talk about IKL; it's a logic with nice Web-like properties such as any collection of well-formed IKL sentences is itself well-formed. As he was talking, I saw lots of parallels to N3... propositions as terms, log:uri, etc.

By Friday night I was exhuasted from travel, lack of sleep, and conference-going, but I couldn't get the IKL/N3 ideas out of my head, so I had to code it up as another output mode of n3absyn.py.

The superman case works, though it's a bit surprising that rdf:type gets contextualized along with superman. The thread continues with the case of "if your homepage says you're vegetarian, then for the purpose of registration for this conference, you're vegetarian". I'm still puzzling over Pat's explanation a bit, but it seems to make sense.

Along with the IKL spec and IKL Guide, Pat also suggests:

• conference call on IKL, including a slideshow and even a recorded talk
• another slightly earlier powerpoint slideshow

In #swig discussion, Tim mentioned he did some writing on labels and rules and OWL which prompted me to flesh out some related ideas I had. The result is a Makefile and four tests with example labels. One of them is:

All resources on example.com are accessible for all users and meet WAI AA guidelines except those on visual.example.com which are not suitable for users with impaired vision.

I picked an XML syntax out of the air and wrote visaa.lbl:

<label
    xmlns="http://www.w3.org/2007/01/lbl22/label"
    xmlns:mobilebp="http://www.w3.org/2007/01/lbl22/mobilebp@@#"
    xmlns:wai="http://www.w3.org/2007/01/lbl22/wai@@#"
    >
  <scope>
    <domain>example.com</domain>
    <except>
      <domain>visual.example.com</domain>
    </except>
  </scope>
  <audience>
    <wai:AAuser />
  </audience>
</label>

And then in testdata.ttl we have:

<http://example.com/pg1simple> a webarch:InformationResource.
 <http://visual.example.com/pg2needsVision> a
webarch:InformationResource.
 :charlene a wai:AAuser.

Then we run the test thusly...

$ make visaa_test.ttl
xsltproc --output visaa.rdf label2rdf.xsl visaa.lbl
python ../../../2000/10/swap/cwm.py visaa.rdf lblrules.n3 owlAx.n3
testdata.ttl \
                --think --filter=findlabels.n3 --n3 >visaa_test.ttl

and indeed, it concludes:

    <http://example.com/pg1simple>     lt:suitableFor :charlene .

but doesn't conclude that pg2needsVision is OK for charlene.

The .lbl syntax is RDF data via GRDDL and label2rdf.xsl. Then owlAx.n3 is rules that derive from the RDFS and OWL specs; i.e. stuff that's already standard. As Tim wrote, A label is a fairly direct use of OWL restrictions. This is very much the sort of thing OWL is designed for. Only the lblrules.n3 bit goes beyond what's standardized, and it's written in the N3 Rules subset of N3, which, assuming a few built-ins, maps pretty neatly to recent RIF designs.

A recent item from Bijan notes a SPARQL-rules design by Axel; I wonder if these rules fit in that design too. I hope to take a look soonish.

A while back, somebody turned the Monty Python Burn the Witch sketch into an example resolution proof. Bijan and Kendall had some fun turning it into OWL.

I'm still finding bugs pretty regularly, but the cwm/n3 proof stuff is starting to mature; it works for a few PAW demo scenarios. Ralph asked me to characterize the set of problems it works for. I don't have a good handle on that, but this witch example seems to be in the set.

Transcribing the example resolution FOL KB to N3 is pretty straightforward; the original is preserved in the comments:

@prefix : <witch#>.
@keywords is, of, a.

#[1] 	BURNS(x) /\ WOMAN(x)	 	=>	WITCH(x)

{ ?x a BURNS. ?x a WOMAN } => { ?x a WITCH }.

#[2]	WOMAN(GIRL)
GIRL a WOMAN.

#[3]	\forall x, ISMADEOFWOOD(x)	=>	BURNS(x)
{ ?x a ISMADEOFWOOD. } => { ?x a BURNS. }.

#[4]	\forall x, FLOATS(x) 		=>	ISMADEOFWOOD(x)
{ ?x a FLOATS } => { ?x a ISMADEOFWOOD }.

#[5]	FLOATS(DUCK)

DUCK a FLOATS.

#[6]	\forall x,y FLOATS(x) /\ SAMEWEIGHT(x,y) =>	FLOATS(y)

{ ?x a FLOATS. ?x SAMEWEIGHT ?y } => { ?y a FLOATS }.

# and, by experiment
# [7]	SAMEWEIGHT(DUCK,GIRL)

DUCK SAMEWEIGHT GIRL.
 

Then we run cwm to generate the proof and then run the proof checker in report mode:

$ cwm.py witch.n3  --think --filter=witch-goal.n3  --why >witch-pf.n3
$ check.py --report witch-pf.n3 >witch-pf.txt 

The report is plain text; I'll enrich it just a bit here. Note that in the N3 proof format, some formulas are elided. It makes some sense not to repeat the whole formula you get by parsing an input file, but I'm not sure why cwm elides results of rule application. It seems to give the relevant formula on the next line, at least:

1. ...
   [by parsing <witch.n3>]
   
   
2. :GIRL a :WOMAN .
   [by erasure from step 1]
   
   
3. :DUCK :SAMEWEIGHT :GIRL .
   [by erasure from step 1]
   
   
4. :DUCK a :FLOATS .
   [by erasure from step 1]
   
   
5. @forAll :x, :y . { :x a wit:FLOATS; wit:SAMEWEIGHT :y . } log:implies {:y a wit:FLOATS . } .
   [by erasure from step 1]
   
   
6. ...
   [by rule from step 5 applied to steps [3, 4]
   with bindings {'y': '<witch#GIRL>', 'x': '<witch#DUCK>'}]
   
   
7. :GIRL a :FLOATS .
   [by erasure from step 6]
   
   
8. @forAll :x . { :x a wit:FLOATS . } log:implies {:x a wit:ISMADEOFWOOD . } .
   [by erasure from step 1]
   
   
9. ...
   [by rule from step 8 applied to steps [7]
   with bindings {'x': '<witch#GIRL>'}]
   
   
10. :GIRL a :ISMADEOFWOOD .
    [by erasure from step 9]
    
    
11. @forAll :x . { :x a wit:ISMADEOFWOOD . } log:implies {:x a wit:BURNS . } .
    [by erasure from step 1]
    
    
12. ...
    [by rule from step 11 applied to steps [10]
    with bindings {'x': '<witch#GIRL>'}]
    
    
13. :GIRL a :BURNS .
    [by erasure from step 12]
    
    
14. @forAll witch:x . { witch:x a :BURNS, :WOMAN . } log:implies {witch:x a :WITCH . } .
    [by erasure from step 1]
    
    
15. ...
    [by rule from step 14 applied to steps [2, 13]
    with bindings {'x': '<witch#GIRL>'}]
    
    
16. :GIRL a :WITCH .
    [by erasure from step 15]
    
    
    

All the files are in the swap/test/reason directory: witch.n3, witch-goal.n3, witch-pf.n3, witch-pf.txt. Enjoy.

In our PAW and TAMI projects, we're making a lot of progress on the practical aspects of proof exchange: in PAW we're working out the nitty gritty details of making an HTTP client (proxy) and server that exchange proofs, and in TAMI, we're working on user interfaces for audit trails and justifications and on integration with a truth maintenance system.

It doesn't concern me too much that cwm does some crazy stuff when finding proofs; it's the proof checker that I expect to deploy as part of trusted computing bases and the proof language specification that I hope will complete the Semantic Web standards stack.

But N3 proof exchange is no longer a completely hypothetical problem; the first examples of interoperating with InferenceWeb (via a mapping to PML) and with Euler are working. So it's time to take a close look at the proof representation and the proof theory in more detail.

My trip to Austin for a research library symposium at the University of Texas gave me a chance to re-connect with Bob Boyer. A while back, I told him about RDF and asked him about Semantic Web logic issues and he showed me the proof checking part of McCune's Robbins Algebras Are Boolean result:

Proofs found by programs are always questionable. Our approach to this problem is to have the theorem prover construct a detailed proof object and have a very simple program (written in a high-level language) check that the proof object is correct. The proof checking program is simple enough that it can be scrutinized by humans, and formal verification is probably feasible.

In my Jan 2000 notes, that excerpt is followed by...

I offer a 500 brownie-point bounty to anybody who converts it to Java and converts the ()'s in the input format to <>'s.

5 points for perl. ;-)

Bob got me invited to the ACL2 seminar this week; in my presentation, Toward proof exchange in the Semantic Web. I reviewed a bit of Web Architecture and the standardization status of RDF, RDFS, OWL, and SPARQL as background to demonstrating that we're close to collecting that bounty. (Little did I know in 2000 that TimBL would pick up python so that I could avoid Java as well as perl ;-)

Matt Kauffman and company gave all sorts of great feedback on my presentation. I had to go back to the Semantic Web Wave diagram a few times to clarify the boundary between research and standardization:

• RDF is fully standardized/ratified
  
• turtle has the same expressive capability as RDF's XML syntax, but isn't fully ratified, and
• N3 goes beyond the standards in both syntax and expressiveness
  

One of the people there who knew about RDF and OWL and such really encouraged me to get N3/turtle done, since every time he does any Semantic Web advocacy, the RDF/XML syntax is a deal-killer. I tried to show them my work on a turtle bnf, but what I was looking for was in June mailing list discussion, not in my February bnf2turtle breadcrumbs item.

They asked what happens if an identifier is used before it appears in an @forAll directive and I had to admit that I could test what the software does if they wanted to, but I couldn't be sure whether that was by design or not; exactly how quantification and {}s interact in N3 is sort of an open issue, or at least something I'm not quite sure about.

Moore noticed that our conjunction introduction (CI) step doesn't result in a formula whose main connective is conjuction; the conjuction gets pushed inside the quantifiers. It's not wrong, but it's not traditional CI either.

I asked about ACL2's proof format, and they said what goes in an ACL2 "book" is not so much a proof as a sequence of lemmas and such, but Jared was working on Milawa, a simple proof checker that can be extended with new prooftechniques.

I started talking a little after 4pm; different people left at different times, but it wasn't until about 8 that Matt realized he was late for a squash game and headed out.

I went back to visit them in the U.T. tower the next day to follow up on ACL2/N3 connections and Milawa. Matt suggested a translation of N3 quantifiers and {}s into ACL2 that doesn't involve quotation. He offered to guide me as I fleshed it out, but I only got as far as installing lisp and ACL2; I was too tired to get into a coding fugue.

Jared not only gave me some essential installation clues, but for every technical topic I brought up, he printed out two papers showing different approaches. I sure hope I can find time to follow up on at least some of this stuff.

del.icio.us tags:Austin, semantic, web, logic, research

Blogged with Flock

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...

The proof generation feature of cwm has been in development for a long time. The idea goes back at least as far as the section on proofs and validation in the original 1998 Semantic Web Roadmap, where we find sees of the proof-based access control idea that is now funded under the policy aware web project:

The HTTP "GET" will contain a proof that the client has a right to the response.

And in the TAMI project, we're looking at proofs as part of an audit mechanism for accountable datamining.

The cwm development process incorprates aspects of extrememe programming: test-driven development and a variation on pair programming; when somebody has a new feature working, somebody else in the group tries to (a) reproduce the test results and (b) review the tests, if not the code. When the pair agree that the tests are OK, we claim victory in a small group setting, and if that goes well, we make a release or at least send mail about the new feature. This typically takes a week or two or three.

In the case of cwm --why, I have been evaluating the tests since at least as far back as this December 2002 check-in comment on swap/test/reason/Makefile, and I still haven't made up my mind:

date: 2002/12/30 15:00:35; author: timbl; state: Exp; lines: +9 -6
--why works up to reason/t5. GK and SBP's list bugs fixed.

I have tried and failed to understand many times when Tim explained the simplicity of the reason proof ontology. I think I'm finally starting to get it. I'm nowhere near being certain it's free of use/mention problems, but I'm starting to see how it works.

The InferenceWeb folks have all sorts of nifty proof browsing stuff, and they're working with us in the TAMI project. In our meeting last August, they explained PML well enough that TimBL started on to-pml.n3, some rules to convert cwm's proof structures to PML. The rest of the integration task has been starved by work on SPARQL and Paulo moving to UTEP and all sorts of other stuff, but we seem to be moving again.

I tried running one of my versioning proofs through to-pml.n3 and then looking at it with the InferenceWeb proof browser, but I haven't got the PML structure right and it doesn't give very detailed diagnostics.

I made some progress by loading one of the PML examples into tabulator (alpha) and loading my swap/reason style proof in there and using the outline view to browse the structure. (It turns out that TimBL started coding the tabulator one day when he was having trouble reading a proof. GMTA ;)I discovered that PML is striped:

• NodeSet
  • isConsequentOf
    • InferenceStep
      • hasAntecedent
        • NodeSet
          • ...

... where the swap/reason ontology just has Step objects and hangs the conclusions off them.

That was the key to some big changes to to-pml.n3. I don't have the output working in the PML browser yet, but Paolo sent me a pointer to a PML primer, which seems to have the remaining clues that I need.

See also: help checking/reading some proof related to versioning? to cwm-talk.