File: OL.in

package info (click to toggle)
ladr 0.0.200902a-2
  • links: PTS
  • area: main
  • in suites: squeeze
  • size: 11,400 kB
  • ctags: 7,168
  • sloc: ansic: 59,953; perl: 1,006; python: 620; makefile: 403; sh: 86; csh: 58; modula3: 13
file content (32 lines) | stat: -rw-r--r-- 514 bytes parent folder | download | duplicates (4) 
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
 
op(400, infix, ^).
op(400, infix, v).

set(print_models_portable).
assign(max_models, -1).     % This means there is no limit.

clauses(theory).

x v y = y v x.
(x v y) v z = x v (y v z).
x v (x ^ y) = x.

x ^ y = y ^ x.
(x ^ y) ^ z = x ^ (y ^ z).
x ^ (x v y) = x.

% Add the following pair for complemented lattice

x v c(x) = 1.
x ^ c(x) = 0.

% Add the following for ortholattice

c(x ^ y) = c(x) v c(y).
c(x v y) = c(x) ^ c(y).
c(c(x)) = x.

% definition of Sheffer Stroke

f(x,y) = c(x) v c(y).

end_of_list.