]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/ng_TPTP/LCL410-1.ma
-ng implemented
[helm.git] / helm / software / matita / contribs / ng_TPTP / LCL410-1.ma
1 include "logic/equality.ma".
2
3 (* Inclusion of: LCL410-1.p *)
4
5 (* -------------------------------------------------------------------------- *)
6
7 (*  File     : LCL410-1 : TPTP v3.2.0. Released v2.5.0. *)
8
9 (*  Domain   : Logic Calculi (Wajsberg Algebras) *)
10
11 (*  Problem  : Alternative Wajsberg algebra definitions *)
12
13 (*  Version  : [AB90] (equality) axioms. *)
14
15 (*  English  :  *)
16
17 (*  Refs     : [FRT84] Font et al. (1984), Wajsberg Algebras *)
18
19 (*           : [AB90]  Anantharaman & Bonacina (1990), An Application of the  *)
20
21 (*           : [Bon91] Bonacina (1991), Problems in Lukasiewicz Logic *)
22
23 (*  Source   : [Bon91] *)
24
25 (*  Names    :  *)
26
27 (*  Status   : Satisfiable *)
28
29 (*  Rating   : 0.00 v3.2.0, 0.33 v3.1.0, 0.00 v2.5.0 *)
30
31 (*  Syntax   : Number of clauses     :   20 (   0 non-Horn;  20 unit;   1 RR) *)
32
33 (*             Number of atoms       :   20 (  20 equality) *)
34
35 (*             Maximal clause size   :    1 (   1 average) *)
36
37 (*             Number of predicates  :    1 (   0 propositional; 2-2 arity) *)
38
39 (*             Number of functors    :    8 (   2 constant; 0-2 arity) *)
40
41 (*             Number of variables   :   35 (   1 singleton) *)
42
43 (*             Maximal term depth    :    5 (   2 average) *)
44
45 (*  Comments :  *)
46
47 (* -------------------------------------------------------------------------- *)
48
49 (* ----Include Alternative Wajsberg algebra axioms *)
50
51 (* Inclusion of: Axioms/LCL002-0.ax *)
52
53 (* -------------------------------------------------------------------------- *)
54
55 (*  File     : LCL002-0 : TPTP v3.2.0. Released v1.0.0. *)
56
57 (*  Domain   : Logic Calculi (Wajsberg Algebras) *)
58
59 (*  Axioms   : Alternative Wajsberg algebra axioms *)
60
61 (*  Version  : [AB90] (equality) axioms. *)
62
63 (*  English  :  *)
64
65 (*  Refs     : [FRT84] Font et al. (1984), Wajsberg Algebras *)
66
67 (*           : [AB90]  Anantharaman & Bonacina (1990), An Application of the  *)
68
69 (*           : [Bon91] Bonacina (1991), Problems in Lukasiewicz Logic *)
70
71 (*  Source   : [Bon91] *)
72
73 (*  Names    :  *)
74
75 (*  Status   :  *)
76
77 (*  Syntax   : Number of clauses    :    8 (   0 non-Horn;   8 unit;   0 RR) *)
78
79 (*             Number of literals   :    8 (   8 equality) *)
80
81 (*             Maximal clause size  :    1 (   1 average) *)
82
83 (*             Number of predicates :    1 (   0 propositional; 2-2 arity) *)
84
85 (*             Number of functors   :    5 (   2 constant; 0-2 arity) *)
86
87 (*             Number of variables  :   10 (   1 singleton) *)
88
89 (*             Maximal term depth   :    5 (   2 average) *)
90
91 (*  Comments : To be used in conjunction with the LAT003 alternative  *)
92
93 (*             Wajsberg algebra definitions. *)
94
95 (* -------------------------------------------------------------------------- *)
96
97 (* -------------------------------------------------------------------------- *)
98
99 (* ----Include Wajsberg algebra AND and OR definitions *)
100
101 (* Inclusion of: Axioms/LCL001-2.ax *)
102
103 (* -------------------------------------------------------------------------- *)
104
105 (*  File     : LCL001-2 : TPTP v3.2.0. Released v1.0.0. *)
106
107 (*  Domain   : Logic Calculi (Wajsberg Algebras) *)
108
109 (*  Axioms   : Wajsberg algebra AND and OR definitions *)
110
111 (*  Version  : [AB90] (equality) axioms. *)
112
113 (*  English  :  *)
114
115 (*  Refs     : [FRT84] Font et al. (1984), Wajsberg Algebras *)
116
117 (*           : [AB90]  Anantharaman & Bonacina (1990), An Application of the  *)
118
119 (*           : [Bon91] Bonacina (1991), Problems in Lukasiewicz Logic *)
120
121 (*  Source   : [Bon91] *)
122
123 (*  Names    :  *)
124
125 (*  Status   :  *)
126
127 (*  Syntax   : Number of clauses    :    6 (   0 non-Horn;   6 unit;   0 RR) *)
128
129 (*             Number of literals   :    6 (   6 equality) *)
130
131 (*             Maximal clause size  :    1 (   1 average) *)
132
133 (*             Number of predicates :    1 (   0 propositional; 2-2 arity) *)
134
135 (*             Number of functors   :    4 (   0 constant; 1-2 arity) *)
136
137 (*             Number of variables  :   14 (   0 singleton) *)
138
139 (*             Maximal term depth   :    4 (   3 average) *)
140
141 (*  Comments : Requires LCL001-0.ax *)
142
143 (* -------------------------------------------------------------------------- *)
144
145 (* ----Definitions of or and and, which are AC  *)
146
147 (* -------------------------------------------------------------------------- *)
148
149 (* ----Include Alternative Wajsberg algebra definitions *)
150
151 (* Inclusion of: Axioms/LCL002-1.ax *)
152
153 (* -------------------------------------------------------------------------- *)
154
155 (*  File     : LCL002-1 : TPTP v3.2.0. Released v1.0.0. *)
156
157 (*  Domain   : Logic Calculi (Wajsberg Algebras) *)
158
159 (*  Axioms   : Alternative Wajsberg algebra definitions *)
160
161 (*  Version  : [AB90] (equality) axioms. *)
162
163 (*  English  :  *)
164
165 (*  Refs     : [FRT84] Font et al. (1984), Wajsberg Algebras *)
166
167 (*           : [AB90]  Anantharaman & Bonacina (1990), An Application of the  *)
168
169 (*           : [Bon91] Bonacina (1991), Problems in Lukasiewicz Logic *)
170
171 (*  Source   : [Bon91] *)
172
173 (*  Names    :  *)
174
175 (*  Status   :  *)
176
177 (*  Syntax   : Number of clauses    :    6 (   0 non-Horn;   6 unit;   1 RR) *)
178
179 (*             Number of literals   :    6 (   6 equality) *)
180
181 (*             Maximal clause size  :    1 (   1 average) *)
182
183 (*             Number of predicates :    1 (   0 propositional; 2-2 arity) *)
184
185 (*             Number of functors   :    7 (   2 constant; 0-2 arity) *)
186
187 (*             Number of variables  :   11 (   0 singleton) *)
188
189 (*             Maximal term depth   :    4 (   2 average) *)
190
191 (*  Comments : Requires LCL001-0.ax LCL001-2.ax *)
192
193 (* -------------------------------------------------------------------------- *)
194
195 (* ----Definitions of and_star and xor, where and_star is AC and xor is C  *)
196
197 (* ---I guess the next two can be derived from the AC of and *)
198
199 (* ----Definition of false in terms of truth  *)
200
201 (* -------------------------------------------------------------------------- *)
202
203 (* -------------------------------------------------------------------------- *)