Additional material for "On the algebra of regular sets"
Michael Winter, Torsten Hahmann, and Michael Gruninger
Accepted by Annals of Mathematics and Artificial Intelligence (AIMA)
Proofs that all other properties follow from the compact equational axiomatization of Stonian p-ortholattices in Section 3.1
Compact equational axiomatization of Stonian p-ortholattices: SPOL.p9.in
Proofs for the remaining properties
L1^, L1v, L2v, L3v, L4^, L4v, L5^, L5v, L6v, PC2, PC3, OC1, OC2, OC3, S1:
SPOL.p9.proof (complete Prover9 output)
Haskell program for verifying Stonian p-ortholattices and the five properties
MainProg.hs
verifies whether a structure is a p-ortholattice (see POrthoLattice.hs);
verifies whether A11, A12, and A13 hold;
checks the five properties: (RP1), (RP2), (M), (S), (D)
POrthoLattice.hs provides functions for checking:
Order structure is a lattice;
Lattice is bounded (greatest and lowest element);
Pseudocomplementation exists for all elements;
Orthocomplementation exists for all elements;
Stone property holds
POFrame.hs
Stonian p-ortholattices:
The input files specify the partial order and the orthocomplement operation, and the main program verifies
that the structures are indeed Stonian p-ortholattices (using POrthoLattice.hs) and whether the five properties hold.
C6 (c6.hs) is a Stonian p-ortholattice (c6.lat),
C12 (c12.hs) is a Stonian p-ortholattice (c12.lat),
C14 (c14.hs) is a Stonian p-ortholattice (c14.lat) satisfying A11, A12, A13, M;
C16 (c16.hs) is a Stonian p-ortholattice (c16.lat) satisfying A11, A12, A13;
C18 (c18.hs) is a Stonian p-ortholattice (c18.lat) satisfying A11, A12, A13, RP1, RP2, M, S, D;
C20 (c20.hs) is a Stonian p-ortholattice (c20.lat) satisfying A11, A12, A13, RP2;
C20d (c20d.hs) is a Stonian p-ortholattice (c20d.lat) satisfying A11, A12, A13, RP1;
C20m (c20m.hs) is a Stonian p-ortholattice (c20m.lat) satisfying A11, A12, A13, RP1, RP2;
C24 (c24.hs) is a Stonian p-ortholattice (c24.lat) satisfying A11, A12, A13, RP1, RP2, M, S, D.
Verification that C14 ∖ {0} is a model of RT0
Theories in Common Logic:
Theory RT-: rtminus.clif
Theory Λ (RT- ∪ {A11, A12, A13} restricted to exactly 13 elements): rt13.clif
13-element model of Λ found by Paradox: rt13.tptp.out
TPTP input (mixed FOF and CNF sentences): rt13.tptp (automatically translated from rt13.clif)
TPTP input (only FOF, for running online on TPTP.org): rt13_fof.tptp