LP

• To: horning@pa.dec.com
• Subject: LP
• From: Michal_Iglewski@uqah.uquebec.ca (Michal Iglewski)
• Date: Fri, 4 Aug 1995 09:56:57 +0500
• Cc: iglewski@saturne.uqah.uquebec.ca
• Delivery-Date: Fri, 04 Aug 95 07:11:51 -0700

Hi Jim,

I decided to use Larch and LP in my course for undergraduated students
(this is the best way to learn something). I have a few small problems.
One of them is the example of your book on p. 141.

FinSet: trait
	introduces
		empty: -> S
		insert: S, E -> S
		singleton: E -> S
		__ \U __: S, S -> S
		__\in __: E, S -> Bool
		__ \subseteq __: S, S -> Bool
	asserts
		S generated by empty, insert
		S partitioned by \in
		\forall s, s1: S, e, e1: E
			singleton(e) == insert(empty, e);
			s \U empty == s;
			s \U insert(s1, e) == insert(s \U s1, e);
			~(e \in empty);
			e \in insert(s, e1) == e \in s \/ e = e1;
			empty \subseteq s;
			insert(s, e) \subseteq s1 == s \subseteq s1 /\ e \in s1
	implies
		S partitioned by \subseteq
		S generated by empty, singleton, \U

According to the text on the same page, if I type LP commands

	execute FinSet_Axioms
	prove sort S partitioned by \subseteq

LP translates the partitioned by into a deduction rule, and then, if I type
complete, LP should finish the proof. However, this is not the case.
It seems to me that the proof of this property is much more complicated.
Am I right?

Michal

• Prev: FWD: CFP for Formal Methods Workshop, ICSE '96 Berlin
• Next: FWD: Dagstuhl specification competition, reactive control systems
• Index: Larch archive index