[Prev][Next][Index]
Re: LSL boolean combinations involving undefined terms
In article <leavens.806079418@bambam.cs.iastate.edu>,
leavens@cs.iastate.edu (Gary Leavens) writes:
|> What I had intended was that the traits specify
|> a function, isPositive that returns true if and only if
|> its argument has tag 'theInt' and is positive.
The three definitions of isPositive (given in the traits Q1, Q2, and
Q3) are equivalent and they fully define isPositive.
|> I think, looking at the trait Boolean in the Larch book,
|> that this is correct. There is a rule in that trait:
|> false /\ b == false,
LSL is defined in terms of a multisorted first-order logic with equality; see
[GHM90, p. 22 and Appendix I]. The Boolean trait is for documentation only.
|> which seems to give the required false when tag(q) = theBool.
|> However, despite the implication (implies AC(/\, Bool) in that trait,
|> I don't see where the commutivity comes from in the axioms,
|> so I still wonder about...
Commutativity can be proven by induction and probably so can associativity.
Patrice
[GHM90] is
@TechReport( Guttag90,
Author = {Guttag, John~V. and Horning, James~J. and Modet, Andr\'es},
Title = {Report on the {L}arch {S}hared {L}anguage: Version 2.3},
Type = {Report},
Number = 58,
Institution = {DEC Systems Research Center},
Address = {Palo Alto, CA},
Month = {April 14},
Year = 1990,
Note = {Superseded by Chapter 4 of \cite{Guttag93}}
)
-------------------------------------------------------------------------------
P. Chalin http://www.cs.concordia.ca/~faculty/chalin
Computer Science Department TEL: (514) 848-3000 FAX: (514) 848-2830
Concordia University E-MAIL: chalin@cs.concordia.ca
1455 de Maisonneuve Boulevard West, Montreal, Quebec, Canada H3G 1M8
-------------------------------------------------------------------------------
Follow-Up(s):
Reference(s):