Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
From: cmere@omega.lncc.br (Maria Claudia Mere)
Message-Id: <9510231318.AA25311@omega.lncc.br>
Subject: HELP!!
To: info-hol@cs.byu.edu
Date: Mon, 23 Oct 1995 11:18:04 -0200 (GRNLNDDT)
Mime-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Length: 995       

Dear Sir/Madam,

I am using the temporal logic S4.3.1 to specify Hypermedia applications,
actually the navegational behaviour of them.
A specification is a theory of first-order, two-sorted formulas in 
such modal logic. We have also, equality for each sort.

1- I would like to know if HOL is an automatic-theorem prover for such logic.
2- What kind of information does HOL need? an Hilbert axiomatic system is
enough or, must  a deductive system (like Sequent Calculus or Natural
Deduction)  be supplied?
3-  I want to prove some properties from the specification (a set of
axioms) of a particular application. Is it easy to enter in HOL the
formulas of each theory? (it will be used by people from Hypermedia )
4- In this case, a specification is a theory (a set of formulas) formed
only with Horn Clauses.
Do you think that this kind of theories would help to reach better
results?

I look forward to hearing from you soon.
Yours faithfully,
Claudia

Maria Claudia Mere
Dra. em Informatica