15 July 2006

• Modified cwm-pml to reflect Li's solution of using SourceUsage for large formula.
  cwm http://dig.csail.mit.edu/TAMI/lkagal/scenario3/scenario3-0715.proof http://www.w3.org/2000/10/swap/reason.n3 http://dig.csail.mit.edu/TAMI/lkagal/cwm-pml/cwm-pml-ver1.n3 --think --filter="http://dig.csail.mit.edu/TAMI/lkagal/cwm-pml/cwm-pml-ver1.n3" --data --rdf > scenario3-0715.pml
• Modified cwm-pml according to Lalana's solution of associating a bnode with its value and displaying it in the same way variables are in IW Browser.
  cwm http://dig.csail.mit.edu/TAMI/lkagal/scenario3/scenario3-0715.proof http://www.w3.org/2000/10/swap/reason.n3 http://dig.csail.mit.edu/TAMI/lkagal/cwm-pml/cwm-pml-ver2.n3 --think --filter="http://dig.csail.mit.edu/TAMI/lkagal/cwm-pml/cwm-pml-ver2.n3" --data --rdf > scenario3-0716.pml

4 July 2006

• Modified cwm-pml.n3 to provide uris for formulae instead of the formulae themselves. This means that each formula appears just once in the pml.
• Changed the schema for iw:Formula. Formula is a class with n3Formula, n3String, and fromFile as properties. NodeSets use the property iw:usesFormula to refer to the formula (iw:formula) and variable (iw:variable) used.

27 June 2006

• Modified cwm-pml.n3 so that additional Extraction from Inference is suppressed.
• View new PML proof in browser

23 June 2006

• Modified cwm-pml.n3 to handle the new proofs that cwm generates in order to suppress the input formula occurring several times in the proof.
  • Inference is the rule used when a formula is used for log:includes or log:notIncludes. An Inference has no antecedents.
  • When a rule uses a formula and has antecedents I use GMP
• Please check out new version of cwm.

15 June 2006

• Cynthia has added functionality to IW browser to display different formats - Raw, N3, and English.
  • Rendered original language. For N3, I just take out namespaces, for now.
  • English. If there is "hasEnglishString" property, its content is shown. Otherwise, if there is an English translator for the conclusion language, the translator translates the conclusion. For N3, we don't have the translator, so the original conclusion is shown.
  • Raw. The original conclusion is shown.
• Vasco has modified the IW Explainer. Example
• cwm-pml.n3 uses Direct Assertion instead of Extraction, Generalized Modus Ponens instead of Inference, and Conjunction Introduction instead of Conjunction.
• Also changed hasLanguage from rein#N3 to http://inferenceweb.stanford.edu/registry/LG/N3.owl#N3 which was required to display the N3 format.
• To Do
  • Scenario3
  • hasEnglishDesc for conclusions

1 June 2006

• hasSourceUsage supports unregistered sources. Fixed by Cynthia.
• cwm-pml.n3 now generates sourceusage for Extraction. Also fixed problem with --filter generating oversimplified results.
• View PML of Example1 in Inference Web
• View PML of Example2 in Inference Web
• Carlos's TAMI scenario 3 : Check if a transfer is legal
  • Ontology, data, and rules
  • Modified Carlos's rules
  • Modified filter
  • N3 Proof
  • PML proof
  • View PML proof in IW
• Scenario 3 : Check if an arrest is justified by ensuring that all antecedents in its antecedent chain are legal/justified.
  • Simple N3 rules
  • Filter
  • Modified data
  • To generate N3 proof :
    cwm http://dig.csail.mit.edu/TAMI/lkagal/cwm-pml/tami-scenario3-data.n3 http://dig.csail.mit.edu/TAMI/cdk/scenario3/schema.n3 http://dig.csail.mit.edu/TAMI/lkagal/cwm-pml/tami-scenario3-rules.n3 --think --filter="http://dig.csail.mit.edu/TAMI/lkagal/cwm-pml/tami-scenario3-filter.n3" --base=foo --why > tami-scenario3.proof
  • N3 Proof
  • To generate PML proof :
    cwm tami-scenario3.proof http://www.w3.org/2000/10/swap/reason.n3 http://dig.csail.mit.edu/TAMI/lkagal/cwm-pml/cwm-pml.n3 --think --filter="http://dig.csail.mit.edu/TAMI/lkagal/cwm-pml/cwm-pml.n3" --rdf > tami-scenario3.pml
  • PML proof
  • View PML proof in IW
• To Do
  • Split conclusion of conjunction to its components
  • Question: Is it possible to have more than 5 for the lens magnitute. Is this required ? It is possible to drill down as required. For example, clicking on an Extraction NodeSet provides all the steps that lead to that Extraction that may not have been displayed in the original proof.