-
Notifications
You must be signed in to change notification settings - Fork 1
/
example.bram
67 lines (65 loc) · 1.96 KB
/
example.bram
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
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<bram> <!-- Document Root -->
<Program>My Logic Program</Program>
<Version>1.0</Version>
<metadata>
<author>Bram van Heuveln</author>
<created>2019-04-25T08:00:00Z</created>
<modified>2019-04-25T15:23:59Z</modified>
<hash>qShJgPT/YKjyO0xVNrelUQrPt7Yofmx8wklDk88Y8Ms=</hash>
<!-- Note: hash is deprecated. See Specifications -->
</metadata>
<proof id="0">
<assumption linenum="0">
<sen>(P \/ Q)</sen>
<!-- Note: sen is depcrated in favor of raw. See Specifications -->
<raw>P v Q #This line means P or Q</raw>
</assumption>
<assumption linenum="1">
<raw>R</raw>
</assumption>
<goal>
<sen>R</sen>
<!-- Note: sen is depcrated in favor of raw. See Specifications -->
<raw>R #Here just for example</raw>
</goal>
<step linenum="2">
<rule>SUBPROOF</rule>
<premise>1</premise>
</step>
<step linenum="4">
<rule>SUBPROOF</rule>
<premise>2</premise>
</step>
<step linenum="6">
<sen>R</sen>
<raw>R</raw>
<rule>DISJUNCTIVE_SYLLOGISM</rule>
<premise>1</premise>
<premise>2</premise>
<premise>4</premise>
</step>
</proof>
<proof id="1">
<assumption linenum="2">
<sen>P</sen>
<raw>P</raw>
</assumption>
<step linenum="3">
<sen>R</sen>
<raw>R</raw>
<rule/>
</step>
</proof>
<proof id="2">
<assumption linenum="4">
<sen>Q</sen>
<raw>Q</raw>
</assumption>
<step linenum="5">
<sen>R</sen>
<raw>R</raw>
<rule/>
</step>
</proof>
</bram>