hets/Hets_input_examples/simpleSentences.het

	simpleSentences.het revision 81f49ee02aaa3bc870401f8883bf52742eb3ea7a


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
logic Hybrid

%% Page 66, Brauner's book on proof theory
%% some axioms

spec Dist1 =
	preds p,q : ()
	modality M
	. [M] (p /\ q) => ([M]p /\ [M]q) %implied
end

spec Test =
        preds p,q : ()
        nominal N
        . (p /\ q)
        . @N p %implied

spec Dist2 =
	preds p,q : ()
	nominal N
	. @N (p /\ q) => (@N p /\ @N q) %implied
end

spec Ref1 =
	nominal N
	. @N (Here N) %implied
end

spec Ref2 =
	. !X (Here X)	%implied
end

spec Scope =
	preds p : ()
	nominals A,B
	. (@A @B p) <=> (@B p) %implied
end

spec Intro =
	preds p : ()
	nominal A
	.  (Here A /\ p) => @A p %implied
end