[Prev][Next][Index][Thread]

Re: Papers available by Public ftp



	Date: Mon, 28 Mar 1994 15:04:37 +1000
	From: Greg Restall <Greg.A.Restall@arp.anu.edu.au>

	The directory contains a file README with short descriptions of the 
	works in the directory.  They include papers on substructural logics,

With regard to your "A Useful Substructural Logic" in that directory,
it is worth mentioning that this logic supports an equational
definition of transitive closure.  See my paper

	@InProceedings(
Pr90b,	Author="Pratt, V.R.",
	Title="Action Logic and Pure Induction",
	Booktitle="Logics in AI: European Workshop JELIA '90, LNCS 478",
	Editor="J. van Eijck", Publisher="Springer-Verlag", Pages="97-120",
	Address="Amsterdam, NL", Month=Sep, Year=1990)

making this point, abstract appended, paper available by anonymous ftp
as boole.stanford.edu:/pub/jelia.tex.

At a talk at a 1992 conference:

        @InProceedings(
Pr92c,  Author="Pratt, V.R.",
        Title="A Roadmap of Some Two-Dimensional Logics",
        Booktitle="Logic and Information Flow", 
        Editor="Van Eijck, J. and Visser, A.", Year="1994")
	(belatedly published only this year due to unplanned change of
	publisher by the organizers)

I identified a number of RA-like logics.  Your Peirce monoids appear on
my chart as the class RES of residuated monoids, while their expansion
with transitive closure is ACT (for action algebras).  This paper is
twod.tex on Boole.

Key to any equational definition of transitive closure is the ability
to express induction, which requires some form of antimonotonicity.
With residuated or Peirce monoids, antimonotonicity is supplied by
residuation (implication).  An alternative source of antimonotonicity
is Boolean negation, which I used much earlier to define transitive
closure equationally in

	@InProceedings(
Pr79c,	Author="Pratt, V.R.",
	Title="Models of program logics",
	Booktitle="20th Symposium on foundations of Computer Science",
	Address="San Juan", Month=Oct, Year=1979)

and

	@InProceedings(
Pr80b,	Author="Pratt, V.R.",
	Title="Dynamic algebras and the nature of induction",
	Booktitle="12th ACM Symposium on Theory of Computation",
	Address="Los Angeles", Month=Apr, Year=1980)

Vaughan Pratt

=============
Abstract:

In Floyd-Hoare logic programs are dynamic while assertions are static
(hold at states).  In action logic the two notions become one, with
programs viewed as on-the-fly assertions whose truth is evaluated along
intervals instead of at states.  Action logic is an equational theory
ACT conservatively extending the equational theory REG of regular
expressions with operations preimplication a -> b (HAD a THEN b) and
postimplication b <- a (b IF-EVER a).  Unlike REG, ACT is finitely
based, makes a* reflexive transitive closure, and has an equivalent
Hilbert system.  The crucial axiom is that of pure induction,
(a -> a)* = a -> a.