RE: OWL semantics ( with focus on an axiomatization)

Chris,

> To my knowledge there is no such proof->code connection for 
> any language except what has been done with kids/specware.

There are many such examples.  Depends on what you consider 
a language.  

The only reason more of this is not done is that almost no 
commercial languages provide the formal underpinning needed 
to construct such proofs.  Which is why our formal semantics 
is so important.  'Build it and they will come'.

- Mike

For some examples of what can be done see
http://www.cs.utexas.edu/users/moore/acl2/acl2-doc.html

Another noteworthy example is the Verdi compiler 
http://www.ora.on.ca/eves.html

I'm kind of out of this area these days, I'm sure there 
is much more going on.

Older work (that I know about because I was involved) 
can be found in

 Journal of Automated Reasoning, Special Issue on 
 System Verification, Vol. 5 No. 4 1989.

which contains a tour de force demonstration of the 
construction of a stack of formally specified and proven 
correct implementations including

1. A hardware instruction set demonstrated to be implemented 
by a gate level chip description (which was fabricated and 
tested, yielding no errors)

2. An assembly language, PITON, formally specified, 
implemented in the above instruction set, and proven correct

3. An operating system, formally specified, implemented 
in PITON, and proven correct

4. A simple high level programming language (microGypsy), 
implemented in PITON (e.g. compiled to PITON),  and 
proven correct.

5. Some simple programs, written in microGypsy, and 
proven correct.

Its hard work, but it is doable.




-----Original Message-----
From: Christopher Welty [mailto:welty@us.ibm.com]
Sent: Tuesday, August 06, 2002 4:22 PM
To: Peter F. Patel-Schneider
Cc: www-webont-wg@w3.org; www-webont-wg-request@w3.org
Subject: Re: OWL semantics ( with focus on an axiomatization)



Peter,

To my knowledge there is no such proof->code connection for any language 
except what has been done with kids/specware. 

Connecting different axiomatizations is possible only given a reliable 
translation between their representations.  It is a theoretical 
possibility, of course, but in practise introduces more sources of 
unreliability.  Intel used a model checker to prove the 486 floating point 
arithmetic worked....yet as we know it didn't.  The breakdown happened 
during translation.

I basically predicted something like this was bound to happen, because the 
formal V&V crowd had been pushing "formal correctness" without requiring 
that the specification that is validated be the specification that 
actually runs.  Should you have more confidence that 150 axioms more 
accurately represents what something does than 1500 lines of code????

Anyway, this is a major tangent.  I just wanted to prevent the claim that 
having an axiomatization proven consistent tells us anything more than it 
does.

-Chris


Dr. Christopher A. Welty, Knowledge Structures Group
IBM Watson Research Center, 19 Skyline Dr.
Hawthorne, NY  10532     USA 
Voice: +1 914.784.7055,  IBM T/L: 863.7055
Fax: +1 914.784.6078, Email: welty@us.ibm.com





"Peter F. Patel-Schneider" <pfps@research.bell-labs.com>
Sent by: www-webont-wg-request@w3.org
08/06/2002 04:51 PM

 
        To:     Christopher Welty/Watson/IBM@IBMUS
        cc:     www-webont-wg@w3.org
        Subject:        Re: OWL semantics ( with focus on an axiomatization)

 


From: "Christopher Welty" <welty@us.ibm.com>
Subject: Re: OWL semantics ( with focus on an axiomatization)
Date: Tue, 6 Aug 2002 16:42:30 -0400

> I'm sure Deborah knows this, but just for the record:
> 
> One can not prove that an axiomatization of a semantics of a language is 

> "correct", only that it is consistent. 

That depends on what you mean by ``correct''.

It is possible to prove that an axiomatization is sound and complete wrt
some other formal specification of entailment, such as a model theory, or
even a different axiomatization. 

> Since there is no hard link 
> between the axiomzatization of the semantics and the actual code that 
> implements those semantics, there is no way to know if the axioms 
> accurately represent the implementation of the reasoner.

> In other words, we have a reasoner like Classic implemented with some 
> code, let's call this "artifact 1".  Then we have a set of axioms that 
> represent the semantics of Classic, let's call this "artifact 2".  We 
can 
> prove that artifact 2 is consisent, i.e. contains no logical 
> contradictions, but we can't prove that it is an accurate representation 

> of artifact 1 [1]

Why not?  Let's assume that the reasoner for Classic is ``implemented'' in
the lambda calculus, to pick an obvious example.  It is possible, but very
hard, to show that a set of axioms in some formal system corresponds to
this ``implementation''.

Of course, any particular LISP system that runs on a physical computer may
not be a correct implementation of the lambda calculus, so there is no
completely-solid connection between the axiomatization and running code.

[...]

> -Chris

peter

Received on Wednesday, 7 August 2002 11:31:57 UTC