Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Mon, 28 Nov 1994 15:36:07 +0000
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA17489;
          Mon, 28 Nov 1994 08:25:23 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from jaguar.cs.byu.edu by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA17475;
          Mon, 28 Nov 1994 08:24:55 -0700
Received: from localhost by jaguar.cs.byu.edu (1.38.193.4/CS-Client) id AA25739;
          Mon, 28 Nov 1994 08:25:31 -0700
Message-Id: <9411281525.AA25739@jaguar.cs.byu.edu>
To: info-hol@leopard.cs.byu.edu
Cc: es2033@eng.warwick.ac.uk
Subject: Forward: rigid body dynamics in HOL
Date: Mon, 28 Nov 1994 08:25:31 -0700
From: Phil Windley <windley@lal.cs.byu.edu>


Hi all,

This message was sent to info-hol-request.  I'm forwarding it to the list.

------- Forwarded Message

From: es2033@eng.warwick.ac.uk
Subject: A question
To: info-hol-request@leopard.cs.byu.edu
Date: Mon, 28 Nov 94 13:06:26 GMT



 Hi,

 I am trying to formulate the theory of rigid body dynamics in HOL.
 While doing this work I asked to myself a question which I couldn,t
 answer.

  - A theory of mechanics(classical) asserts the existence of an inertial
    coordinate system. The existence of this coordinate system is based on
    experiments. Can one define such an inertial coordinate system in HOL?

 This question, I think, will occur to anyone trying to formalize any 
 physical theories. Any comments will be most welcomed.

 Yours sincerely

 Nam :es2033@eng.warwick.ac.uk
  

------- End of Forwarded Message