Xref: utzoo sci.logic:915 comp.theory:910
Path: utzoo!attcan!uunet!mcsun!ukc!edcastle!lfcs!hans
From: hans@lfcs.ed.ac.uk (Hans Huttel)
Newsgroups: sci.logic,comp.theory
Subject: Conditional equational reasoning - reference(s) wanted
Summary: There is more to equational logic than `A is A'...
Keywords: sequents,equations
Message-ID: <5460@castle.ed.ac.uk>
Date: 1 Aug 90 13:38:00 GMT
Reply-To: hans@lfcs.ed.ac.uk (Hans Huttel)
Followup-To: sci.logic
Organization: Laboratory for the Foundations of Computer Science, Edinburgh U
Lines: 30

Can someone out there supply me with some good references on
conditional equational reasoning ? What I am thinking of are
formulations of equational logics going beyond Prawitz in the sense
that hypotheses are involved. More precisely, I am thinking of sequent
calculi (+ related notions) where the sequents are of the form

        H |-  A = B

and a hypothesis H is of the form (A1,B1),...,(An,Bn) interpreted as
assuming the identities A1 = B1,...,An = Bn .

This must have something to do with e.g. the theory of logic programming
(and term rewriting in general, of course). The reason for my interest
in this, however, is that I am looking at possible axiomatizations
of/tableau systems for behavioural equivalences for certain classes of
labelled transition systems in the theory of process algebras.

Please reply by e-mail; if there is interest I will post a summary.


Regards


Hans


Hans H\"{u}ttel, Office 1603        JANET: hans@uk.ac.ed.lfcs
Lab. for Foundations of Comp. Sci.  UUCP:  ..!mcvax!ukc!lfcs!hans
University of Edinburgh             ARPA: hans%lfcs.ed.ac.uk@nsfnet-relay.ac.uk
Edinburgh EH9 3JZ, SCOTLAND         Ain't gonna work on Maggie's farm no more