Manual

(Last modified: 20040910)

back

Acknowledgement
Introduction
Expressions
- Output of program
- OR on the side of conclusions problem
Function references
Priority of the operators and representation in RPN
Examples of usage

Acknowledgement

I would like to thank to the following persons and institutions:

M. Navara for introducing me to the graphical method for computation in free orthomodular lattices
The CEEPUS exchange program mainly to the CEEPUS network no. SK-0042
The host institution of my CEEPUS stay: The Center for Machine Perception of the Faculty of Electrical Engineering of the Czech Technical University

toc

Introduction

toc

This program implements Navara's graphical method for evaluating expressions in orthomodular lattices (OMLs in short) ([1]). This method allows to check in simple way whether some identities hold in OMLs. Not every identity can be checked by this method. The following restrictions are applied:

If the identity contains up to two variables, it can be evaluated by this method without any restriction. (In this case we use the computation in the free orthomodular lattice generated by two generators denoted F(a,b). These generators are denoted by a and b in the program. This lattice has 96 elements and its structure can be depicted by images. For more details, see [1] for the method for creating such images and [1], [2] for the structure of this lattice.)

For identities with more than two variables, there should be only one pair of incompatible elements and all other elements commute with every element in the lattice. Such commutative elements are denoted as ci in the program. ( This restriction is because the free OML with more than 2 generators need not be finite. These commutative elements cause that the structure of the OML can be expressed as a direct product of 2ⁿ copies of F(a,b), where n is the number of compatible elements ci. For more information see [1].)

References

Navara, M., On generating finite orthomodular sublattices, Tatra Mt. Math. Publ. 10 (1997), 3-20
Beran, L., Orthomodular Lattices, Algebraic Approach, Academia 1984, Praha
Pavicic, M., Megill, N., D., Quantum and classical implication, Algebras with primitive implications, Int. J. Th. Physics, 37 (1998), 2091-2098 - used for the expressions for implications

toc

Expressions

toc

Types of expressions which can be evaluated by the program:

Polynomial expressions in OMLs: An expression containing variables (a|x, b|y) or constants (0, 1, B1(<num>) - an element with Beran's number equal to <num>) to which the operations are applied: complement ('), join (j or v), meet (m or ^), skew join (sj or sv), skew meet (sm or s^), Sasaki projection (sp), implications 0-5 (i0, i1, i2, i3, i4, i5), the right-side of the commutativity relation (oC), i.e. a oC b = (a ^ b) v (a ^ b'), the right-side of the dual commutativity relation (oD), i.e. a oD b = (a v b) ^ (a v b'), the lower commutator (lc), a lc b = (a ^ b) v (a ^ b') v (a' ^ b) v (a' ^ b'), the upper commutator (uc), a uc b = (a v b) ^ (a v b') ^ (a' v b) ^ (a' v b') and function B3(<num>, <arg_a>, <arg_b>) - the value is equal to the expression defined by Beran's number <num>, where variable a has value <arg_a> and variable b has value <arg_b>.
The return value is the atomic representation of the element expressed in Navara's graphical representation, plain TeX macro and its Beran's number.
Relations in OML: It can be checked whether expr1 R expr2 holds, where R is one of the following relations: equality (=), less than or equal to (<=), greater than or equal to (>=) and commutativity (C), i.e. equality of the expr1 and expr1 oC expr2. Logical connectives And (AND) and Or (OR) can be used to form compound relation expressions.
The return value of these operations is True or False.
Implications and Equivalences: The validity of implications (=>) and equivalences (<=>) can be also tested. The program accepts the following syntax:
rel1 IMEQ rel2,
where rel1, rel2 are relations
(Note restriction for using OR on the side of conclusions!) (see)
and IMEQ is one of the => or <=>. Semantics of such expression is if rel1, then rel2 for implication and rel1 if and only if rel2 for equivalence.
The return value of these relations is True or False.
Note: For ensuring correct evaluation of the expression always check the Reverse Polish Notation (RPN).

toc

Output of the program

toc

The example of output for the expression a v b: (line numbers added for referring)

    No.of.gen: 0 <-  Number of elements ci
    RPN: abv     <-  Reverse Polish Notation of the expression
     -------     \ 
    |   o   |     \
    | x   x |      - Navara's graphic representation (see [1])
    |   x   |     /
     -------     /
    \nc0111||    <-  TeX macro for typesetting the graphical representation (foml2.sty)
    Beran's number of the element:  92 <- Beran's number of the expression (see [2])

If the number of the elements ci is not equal to 0, then the output contains comma separated list of graphic representations, TeX macros and Beran's numbers of the expression, as shown below.

    No.of.gen: 2
    RPN: c1b^c2a^v
                                         -------
        o       |   o           o   |   |   o   |
      o   o   , | x   o   ,   o   x | , | x   x |
        o       |   x           x   |   |   x   |
                 -------     -------     -------
    \nc0000--, \nc0101|_, \nc0011_|, \nc0111||
    Beran's numbers of components:   1,  22,  39,  92

toc

OR on the side of conclusion problem:

toc

if (a = a), then (a = a ^ (a ^ b)') or (a = a ^ (a ^ b')') (True implies False, i.e. False)

a = a => a = (a ^(a ^b)') OR a = (a ^(a^b')')

Program replies True, however the expression is false.

For details see: (*) Hyčko, M., Implications and Equivalences in Orthomodular Lattices, (submitted).

toc

Function references: Computations in OML

toc

Name Syntax Example of usage

Evaluating expressions:

Constants:

Zero 0 0

Unit 1 1

Element with Beran's number B1(<num>), 1 <= <num> <=96 B1(13), B1(55)

Variables:

Element a (1st element of noncompatible pair) a or x a

Element b (2nd element of noncompatible pair) b or y b

Element ci (compatible with each element) ci, 1<=i<=no_of_comp or c for c1 c, c1, c5

Unary operators:

Complement expr ' a', avb', (avb)'

Binary operators:

Join expr1 v expr2 or expr1 j expr2 a'vb'

Meet expr1 ^ expr2 or expr1 m expr2 a'^b

Skew join - (a ^ b') v b expr1 sv expr2 or expr1 sj expr2 a sv b

Skew meet - (a v b') ^ b expr1 s^ expr2 or expr1 sm expr2 a s^ b

Sasaki projection
\varphi_{expr1}(expr2) = expr1 ^ (expr1' v expr2) expr1 sp expr2 a sp b

Lower commutator expr1 lc expr2 a lc b

Upper commutator expr1 uc expr2 a uc b

Implications:

Classical: expr1' v expr2 expr1 i0 expr2 a i0 b

Sasaki: expr1' v (expr1 ^ expr2) expr1 i1 expr2 a i1 b

Dishkant: expr2 v (expr1' v expr2') expr1 i2 expr2 a i2 b

Kalmbach:
((expr1' ^ expr2) v (expr1' ^ expr2') v
(expr1 ^ (expr1' v expr2)) expr1 i3 expr2 a i3 b

Non-tollens:
((expr1 ^ expr2) v (expr1' ^ expr2)) v
((expr1' v expr2) ^ expr2') expr1 i4 expr2 a i4 b

Relevance:
((expr1 ^ expr2) v (expr1' ^ expr2)) v
(expr1' ^ expr2') expr1 i5 expr2 a i5 b

Right side of Commutativity relation: (expr1 ^ expr2) v (expr1 ^ expr2') expr1 oC expr2 a oC b

Right side of Dual Commutativity relation: (expr1 v expr2) ^ (expr1 v expr2') expr1 oD expr2 a oD b

Functions: <fun>(arg1, arg2, ...)

B3 B3(<num>, <arg_a>, <arg_b>),
1 <= <num> <= 96,
<arg_a>, <arg_b> - expressions
(not relations and if, iff) B3(23,a^b, (avb)')
Relations: Tests whether expr1 R expr2

Equality expr1 = expr2

Less than or equal to expr1 <= expr2

Greater than or equal to expr1 >= expr2

Commutativity C expr1 C expr2

AND rel1 AND rel2

OR rel1 OR rel2
DO NOT USE ON THE SIDE OF CONCLUSIONS !

If/Iff expressions: rel1 < '=>' | '<=>' > rel2

if expression rel1 => rel2 a<=b=>a C b: a = b => a C b

if and only if expression rel1 <=> rel2 a C b <=> b C a': a C b <=> b C a'

Name	Syntax	Example of usage
Evaluating expressions:
Constants:
Zero	0	0
Unit	1	1
Element with Beran's number	B1(<num>), 1 <= <num> <=96	B1(13), B1(55)
Variables:
Element a (1st element of noncompatible pair)	a or x	a
Element b (2nd element of noncompatible pair)	b or y	b
Element ci (compatible with each element)	ci, 1<=i<=no_of_comp or c for c1	c, c1, c5
Unary operators:
Complement	expr '	a', avb', (avb)'
Binary operators:
Join	expr1 v expr2 or expr1 j expr2	a'vb'
Meet	expr1 ^ expr2 or expr1 m expr2	a'^b
Skew join - (a ^ b') v b	expr1 sv expr2 or expr1 sj expr2	a sv b
Skew meet - (a v b') ^ b	expr1 s^ expr2 or expr1 sm expr2	a s^ b
Sasaki projection \varphi_{expr1}(expr2) = expr1 ^ (expr1' v expr2)	expr1 sp expr2	a sp b
Lower commutator	expr1 lc expr2	a lc b
Upper commutator	expr1 uc expr2	a uc b
Implications:
Classical: expr1' v expr2	expr1 i0 expr2	a i0 b
Sasaki: expr1' v (expr1 ^ expr2)	expr1 i1 expr2	a i1 b
Dishkant: expr2 v (expr1' v expr2')	expr1 i2 expr2	a i2 b
Kalmbach: ((expr1' ^ expr2) v (expr1' ^ expr2') v (expr1 ^ (expr1' v expr2))	expr1 i3 expr2	a i3 b
Non-tollens: ((expr1 ^ expr2) v (expr1' ^ expr2)) v ((expr1' v expr2) ^ expr2')	expr1 i4 expr2	a i4 b
Relevance: ((expr1 ^ expr2) v (expr1' ^ expr2)) v (expr1' ^ expr2')	expr1 i5 expr2	a i5 b
Right side of Commutativity relation: (expr1 ^ expr2) v (expr1 ^ expr2')	expr1 oC expr2	a oC b
Right side of Dual Commutativity relation: (expr1 v expr2) ^ (expr1 v expr2')	expr1 oD expr2	a oD b
Functions:	<fun>(arg1, arg2, ...)
B3	B3(<num>, <arg_a>, <arg_b>), 1 <= <num> <= 96, <arg_a>, <arg_b> - expressions (not relations and if, iff)	B3(23,a^b, (avb)')
Relations:	Tests whether expr1 R expr2
Equality	expr1 = expr2
Less than or equal to	expr1 <= expr2
Greater than or equal to	expr1 >= expr2
Commutativity C	expr1 C expr2
AND	rel1 AND rel2
OR	rel1 OR rel2	DO NOT USE ON THE SIDE OF CONCLUSIONS !
If/Iff expressions:	rel1 < '=>' \| '<=>' > rel2
if expression	rel1 => rel2	a<=b=>a C b: a = b => a C b
if and only if expression	rel1 <=> rel2	a C b <=> b C a': a C b <=> b C a'

toc

Priority of operations and representation in RPN

toc

Operators with same priority use left associativity, i.e. a v b v c = (a v b) v c.

(Character ~ means space)

Operator	RPN	Inverse priority (0=highest)
'	`'`	10
sp	`sp`	40
lc	`lc`	40
uc	`uc`	40
^	`^`	50
s^	`s^`	50
v	`v`	100
sv	`sv`	100
i0	`i0`	110
i1	`i1`	110
i2	`i2`	110
i3	`i3`	110
i4	`i4`	110
i5	`i5`	110
oC	`oC`	120
oD	`oD`	120
=	`=~`	200
<=	`<=`	200
>=	`>=`	200
C	`C`	200
AND	`A`	250
OR^!	`O`	275
=>	`if~`	300
<=>	`iff`	300
Constant
0	`0`
1	`1`
B1(.)	`B1`
Integer 1<= <n> <=96	`I<0n>~`	<0n> - an extension of one digit number to two digit number with 0 prefix, i.e. 5 ---> 05
Variable
a	`a`
x	`a`
b	`b`
y	`b`
c	`c1`
c1	`c1`
c2	`c2`
c3	`c3`
c4	`c4`
c5	`c5`
c6	`c6`
c7	`c7`
c8	`c8`
c9	`c9`
Function
B3	`B3`

toc

Examples of usage

toc

Ex.1: To check the validity of the Foulis-Holland theorem:

If c is compatible to a and b then a v (b ^ c)=(a v b) ^ ( a v c), a ^ (b v c) = (a ^ b) v (a ^ c),

we need to set number of commutativity elements to 1 (*NEW* or use the Automatic detection, i.e. A) and as an OML expression input:

a v (b ^ c) = (a v b) ^ (a v c) a ^ (b v c) = (a ^ b) v (a ^ c)

Ex.2: Beran: VII.7 Corollary 7.7:
Under assumption (*)(aCb, bCc) the following conditions are equivalent:
(i) a ^ (b v c) <= a sv c
(ii) a s^ c <= a v (b' ^c)
(iii) L=R, where L = a s^ (b sv c), R = (a s^ b) sv (a s^ c)

To check this corollary, first we have to rename the variables in identities: b is compatible to all elements, so b should be renamed to c and c should be renamed to b. Then we get:
(i) a ^ (c v b) <= a sv b
(ii) a s^ b <= a v (c' ^ b)
(iii) L = R, where L = a s^(c sv b), R = (a s^ c) sv (a s^ b)
We can choose several methods for checking:
(i) <=> (ii), (ii) <=> (iii)
In program:

a ^ (c v b) <= (a sv b) <=> a s^ b <= a v (c' ^b)
a s^ b <= a v (c' ^b) <=> a s^(c sv b) = (a s^ c) sv (a s^ b)

Alternatively, we can use the standard cyclic implication method:
(i)=>(ii)=>(iii) =>(i)
In program:

a ^ (c v b) <= (a sv b) => a s^ b <= a v (c' ^b)
a s^ b <= a v (c' ^b) => a s^(c sv b) = (a s^ c) sv (a s^ b)
a s^(c sv b) = (a s^ c) sv (a s^ b) => a ^ (c v b) <= (a sv b)

toc

back