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