From: Jim Hendler (jhendler@darpa.mil)
Date: 07/13/01
Stefan asked us to provide examples of what we would like to do with
a rule language. I've put together the following example -- first,
I define an ontology that is useful for the expression of proofs
(based on traditional notation schemes from philosophical logic). I
then have rules expressed in various documents, and want a system
that can put them together into a proof document (i.e. an
instantiated proof) that could be checked by some other system. Of
course, I also want this embedded on the web (i.e. URIs used where
possible, etc.)
Richard Fikes is also working on a proof ontology, so I've cc'ed him
in this message.
Some caveats
The current example is almost exclusively in RDF(S) - my plan had
been to do it in RDFS and then in DAML to show the added power of
DAML - I still hope to do that, but just haven't found time.
I have purposefully left all the rules as simply strings, which
express propositional logic (variables and the like should be easily
recognized). I do NOT propose that this is the right way to do it --
rather, I did this to make it easy to see what sort of rules I would
like, and to make it so I could plug in various rule contenders to
see if they would do what I need.
Here we go (following is in RDF/N3 - I merged a set of files quickly,
and so I don't promise there are no syntax violations - but this
should be enough to convey the idea).
---------
@prefix dc: <http://purl.org/dc/elements/1.1/>.
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax#>.
@prefix daml: <http://www.daml.org/2001/03/daml+oil#> .
<> dc:description """
Idea: There is a standard way that students are taught for the exchange of
FOL proofs in philosophical logic courses (like the one I took in 1975 -
ouch!) One generates a proof by showing that a particular set of assumptions
can lead to a particular conclusion via a set of proof steps permitted by
the axioms of FOL. (Propositional cases are easier to show than Predicate,
but same thing works for full FOL).
The idea is simple - each step of a proof is made up of
1. The set of assumptions on which a step depends
2. A step number (or arbitrary label)
3. A new assertion
4. The logical axiom on which it depends
5. The previous step numbers (labels) that were used by the axiom
6. Comments (real logicians don't use comments)
------------------------------------------------------------------------
Example:
Given:
A -> B
B -> -C
C
Prove:
-A
PROOF:
1 (1) A -> B A 1
2 (2) B -> -C A 2
3 (3) C A 3
4 (4) A A 4 ; an assumption is added to
make the proof hold
1,4 (5) B MP 1,4 ; modus ponens of 1,4
1,2,4 (6) -C MP 2,5 ; note assumption 4 included
since 5 was needed
1,2,3,4 (7) C & -C &-I 3,6 ; and-introduction brings in 3
1,2,3 (8) -A RAA 7 ; we can negate any assumption
(we chose 4) by reducio
Thus we see -A dependent only on 1,2,3 and are done.
------------------------------------------------------------------------
Bringing this to the web
The idea is simply to create an ontology which has proof as a class with a
set of statements, each statement containing the stuff above.
------------------------------------------------------------------------
""".
@prefix : <proof-ontology#>.
@prefix Proof: <proof-ontology#>.
:Proof :a rdfs:Class.
Proof:Body :a rdf:Property;
rdfs:domain Proof:Proof;
range [ :collectionOf Proof:Step]. # collectionOf shorthand for Dan's stuff
Proof:Step a rdfs:Class.
:AssumptionSet a rdf:Property;
rdfs:domain Proof:Step;
rdfs:range [ :collectionOf :StepID].
:StepID a daml:UniqueProperty;
rdfs:domain Proof:Step;
rdfs:range :STRING. # how would one do unique property in RDFS?
Proof:Assertion a rdfs:Class.
Proof:AsBody a rdf:Property;
rdfs:domain Proof:Assertion;
rdfs:range :STRING. #
:StepAssertion a rdf:Property;
rdfs:domain Proof:Step;
rdfs:range Proof:Assertion.
:RuleName a rdfs:Class. # IMPORTANT: RuleName can be any URI!
:StepRule :a rdf:Property;
rdfs:domain :ProofStep;
rdfs:range :RuleName.
:StepDependsOn a rdfs:Property;
rdfs:domain :ProofStep;
rdfs:range [ :collectionOf :StepID].
:ResourceDescription a rdfs:class;
:TrustedResource a rdfs:class.
:TrustedLogic a rdfs:class.
:CompoundAssertion a rdfs:Class.
:AssertStep a rdf:property;
rdfs:range CompoundAssertion;
rdfs:Domain [ :CollectionOf :Assertion].
<> dc:description """
Below is an example in which a proof is created from distributed sites.
Note that the actual rules are simply in strings - this is not to imply this
is how to do it, but as examples of what the rule language should allow.
At the Site Granting Access (SITE1): we say a resource is accessible
by X if X is MyMember, or one of my members says X is authorized.
""".
@prefix Proof: <proof-ontology#>.
@prefix : <#>.
:Assert1 a Proof:Assertion;
Proof:AsBody "MyMember(URI1)".
:Rule1 a Proof:Assertion;
Proof:AsBody "MyMember(x) AND AuthBy (user,x) -> Accessible(<>,user)"
<URI1> a Proof:TrustedResource.
<PropLogic> a Proof:TrustedLogic.
<> dc:description """
At URI1 : My employees are authorized and so are recognized
substitutes, John is an employee.
""".
@prefix Proof: <proof-ontology#>.
@prefix : <#>.
:Assert1 a Proof:Assertion;
Proof:AsBody "Employee(JOHN)".
:Rule1 a Proof:Assertion;
Proof:AsBody "Employee(x) -> AuthBy(x,URI1)"
:Rule2 a Proof:Assertion;
Proof:AsBody "Substitute(x,y) AND AuthBy(x,UTI1) -> AuthBy(y,URI1)"
<URI2> a Proof:TrustedResource.
<> dc:description """
At URI2: Mary is allowed to substitute for John
""".
:Assertion1 a Proof:Assertion;
Proof:AsBody "Substitute(JOHN,MARY)";
<> dc:description """
At PropLogic:
""".
@prefix Proof: <proof-ontology#>.
@prefix : <#>.
:ModusPonens a Proof:RuleName.
:AndIntro a Proof:RuleName.
:RuleCitation a Proof:RuleName.
:AssumptionCitation a Proof:Rulename.
<> dc:description """
------------------------------------------------------------------------
The following proof could then be validated by a proof checker at SITE1:
""".
@prefix Proof: <proof-ontology#>.
@prefix : <#>.
@prefix PropLogic: <PropLogic#>.
@prefix U1: <URI1#>.
@prefix U2: <URI2#>.
:ExampleProof a Proof:Proof;
Proof:Body
(PF1 PF2 PF3 PF4 PF5 PF6 PF7 PF8 PF9 PF10 PF11).
:PF1 a Proof:Step;
Proof:AssumptionSet (:PF1);
Proof:StepID "PF1";
Proof:StepAssertion SITE1:Assert1;
Proof:StepRule PropLogic:AssumptionCitation;
Proof:StepDependsOn (:PF1).
:PF2 a Proof:Step;
:AssumptionSet (:PF2);
Proof:StepID "PF2";
Proof:StepAssertion U1:Assert1;
Proof:StepRule PropLogic:AssumptionCitation;
Proof:StepDependsOn (:PF2).
:PF3 a Proof:Step;
Proof:AssumptionSet (:PF3);
Proof:StepID "PF3";
Proof:StepAssertion U2:Assertion1;
Proof:StepRule PropLogic:AssertionCItation;
Proof:StepDependsOn (:PF3).
:PF4 a Proof:Step;
Proof:AssumptionSet (:PF4);
Proof:StepID "PF4";
Proof:StepAssertion U1:Rule1;
Proof:StepRule PropLogic:RuleCItation;
Proof:StepDependsOn (:PF4).
:Conclusion1 a Proof:Assertion;
Proof:AsBody "Auth(John,URI1)";
:PF5 a :ProofStep;
Proof:AssumptionSet (:PF2 PF4);
Proof:StepID "PF5";
Proof:StepAssertion :Conclusion1;
Proof:StepRule PropLogic:ModusPonens;
Proof:StepDependsOn (:PF2 :PF4).
:Compound1 a Proof:AndAssertion;
Proof:AssertSet (U2:assertion1 :Conclusion1).
:PF6 a Proof:Step;
Proof:AssumptionSet (:PF2 :PF3 :PF4);
Proof:StepID "PF6";
Proof:StepAssertion :Compound1;
Proof:StepRule PropLogic:AndIntro; # Rules by URI is web power at its best
Proof:StepDependsOn (:PF3 :PF5).
:PF7 a Proof:Step;
Proof:AssumptionSet (PF7) ;
Proof:StepID "PF7";
Proof:StepAssertion U1:Rule2;
Proof:StepRule PropLogic:RuleCitation;
Proof:StepDependsOn (:PF7).
:Conclusion2 a Proof:Assertion;
Proof:AsBody "AuthBy(Mary,URI1)".
:PF8 a Proof:Step;
Proof:AssumptionSet (:PF2 :PF3 :PF4 :PF7);
Proof:StepID "PF8";
Proof:StepAssertion :Conclusion2;
Proof:StepRule PropLogicModusPonens;
Proof:StepDependsOn (:PF6 :PF7).
:Compound2 a Proof:AndAssertion;
Proof:AssertStep (:Conclusion2 SITE1:Assert1).
:PF9 a Proof:Step;
Proof:AssumptionSet (:PF1 :PF2 :PF4 :PF6 :PF7) ;
Proof:StepID "PF9";
Proof:StepAssertion :Compound2;
Proof:StepRule PropLogic:AndIntro;
Proof:StepDependsOn (:PF1 :PF8).
:PF10 a Proof:Step;
Proof:AssumptionSet (:PF10) ;
Proof:StepID "PF10";
Proof:StepAssertion Site1:Rule1 ;
Proof:StepRule PropLogic:RuleCitation ;
Proof:StepDependsOn (:PF10).
:PF11 a Proof:Step;
Proof:AssumptionSet (:PF1 :PF2 :PF3 :PF4 :PF7 :PF10);
Proof:StepID "PF11";
Proof:StepAssertion :ProvenAssertion;
Proof:StepRule PropLogic:ModusPonens;
Proof:StepDependsOn (:PF9 :PF10).
:ProvenAssertion a Proof:Assertion;
Proof:AsBody "Accessible(<>, Mary)".
<> dc:description """
QED.
Lots of detail stuff left to do - but it actually works!
""".
--
Prof. James Hendler Program Manager
DARPA/ISO 703-696-2238 (phone)
3701 N. Fairfax Dr. 703-696-2201 (Fax)
Arlington, VA 22203 jhendler@darpa.mil
This archive was generated by hypermail 2.1.4 : 04/02/02 EST