Rules and proofs - examples

From: Jim Hendler ([email protected])
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		[email protected]


This archive was generated by hypermail 2.1.4 : 04/02/02 EST