Basic laws on relations proved automatically with

Andrea Formisano, Università degli Studi di L'Aquila, Dipartimento di Informatica

and

Eugenio G. Omodeo, Università degli Studi di Trieste, Dipartimento di Matematica e Informatica

• Kernel

  	pdf	Statements	Test files	Proofs
  Axioms	ax	1_2booleanAx 3booleanAx 3robbinsAx peirceanAx0 peirceanAx1 peirceanAx2 simplicityAx
  Definitions	def	uzDef nDef dDef iDef
  Verifications	layer0   boo	xxxii xxxiii boolEQrobbins 1To4booleanLaws 4To8booleanLaws 9_10booleanLaws 11booleanLaws 12booleanLaws 13booleanLaws 14booleanLaws 15_16booleanLaws 17To19booleanLaws 20To24booleanLaws 25booleanLaws 26_27booleanLaws 28booleanLaws 29booleanLaws (booleanLaws)	robbins xxxii xxxiii boolean	robbins1 robbins2 xxxii xxxiii boolean1 boolean2 boolean3 boolean4 boolean5 boolean6 boolean7 boolean8 boolean9 boolean10 boolean11a boolean11b boolean12 boolean13 boolean14a boolean14b boolean15 boolean16a boolean16b boolean17 boolean18 boolean19 boolean20 boolean21a boolean21b boolean22 boolean23 boolean24 boolean25 boolean26 boolean27 boolean28 boolean29

  (typical values for the search parameters), (extreme option)

• Layer 1 (Laws immediate or almost so from the axioms)

  	pdf	Statements	Test files	Proofs
  Definitions
  Verifications	layer1	i ii iii iv v ix_a ix_b xi_a xi_b xiii xiv xx xxii xxv vi vii 1To3monotLaws 4_5monotLaws (monotLaws) 30booleanLaws	i ii iii iv v  -  ix xi_a xi_b xiii xiv xx xxii xxv vi_vii 1To3monot 4_5monot 30boolean	i0 i1 i2 i3 i4 i5 i6 i7a i7b i7c ii0 ii1To4 iii1 iii2 iii3 iii4 iv1 iv2 v1 v2 ix1 ix2 ix3 ix4 ix5 ix6 ix7 ix8 xi4 xi1 xi3 xi2 xiii4 xiii3 xiii2 xiii1 xiv1 xiv2 xiv3 xiv4 xx1 xx2 xxii2 xxii1 xxv vi1 vi2 vii1 vii2 vii3 vii4 vii5 monot1 monot2 monot3 monot4 monot5 boolean30

• Layer 1.5 (Prelude to Schröder's equivalences)

  	pdf	Statements	Test files	Proofs
  Definitions
  Verifications	layer1.5	cycleLaw	cycle	cycleLaw

• Layer 2 (Laws relying on isotony and the above prelude)

  	pdf	Statements	Test files	Proofs
  Definitions
  Verifications	layer2	viii x_a x_b xii xvii_b xxvi	viii x_a x_b xii xvii_b xxvi	viii x1 x2 xii1 xii2 xvii2 xvii3 xxvi

• Layer 2.5 (Cousins of Schroöder's equivalences)

  	pdf	Statements	Test files	Proofs
  Definitions
  Verifications	layer2.5	cycleLawA cycleLawsB cycleLawC	cycleLawA cycleLawsB cycleLawC	cycleLawA cycleLawsB1 cycleLawsB2 cycleLawsB3 cycleLawC

• Layer 3 (Dedekind's law and its associates)

  	pdf	Statements	Test files	Proofs
  Definitions
  Verifications	layer3	xv_a_ghost xv_a xv_b xvii_a xviii_ghost xviii xix_a_ghost xix_b_ghost xix xxi_a_ghost xxiv_a xxiv xxvii_a_ghost xxvii_a xxvii_b_ghost xxvii xxix_ghost xxix_b_ghost xxix xxxi_ghost xxxi	xv_a_ghost xv_a xv_b xvii_a xviii_ghost xviii xix_a_ghost xix_b_ghost xix xxi_a_ghost xxiv_a xxiv xxvii_a_ghost xxvii_a xxvii_b_ghost xxvii xxix_ghost xxix_b_ghost xxix xxxi_ghost xxxi	xv_a_ghost1 xv_a_ghost2 xv_a0 xv_a1 xv1 xv2 xvii1 xviii_ghost1 xviii_ghost2 xviii xix_a_ghost1 xix_a_ghost2 xix_a_ghost3 xix_a_ghost4 xix_b_ghost1 xix_b_ghost2 xix_b_ghost3 xix_b_ghost4 xix1 xix2 xxi_a_ghost1 xxi_a_ghost2 xxi_a_ghost3 xxiv_a1 xxiv_a2 xxiv  - - - - - - -  xxvii_a xxvii1 xxvii_b_ghost1 xxvii_b_ghost2 xxvii_b_ghost3 xxvii2 xxix_ghost1 xxix_ghost2 xxix_b_ghost xxix xxxi_ghost xxxi

• Layer 3.5 (Prelude to laws xxiii)

  	pdf	Statements	Test files	Proofs
  Definitions
  Verifications	layer3.5	subId_ghost subIdBis_ghost subId_a_ghost subId_Laws_a subId_Laws_b	subId_ghost subIdBis_ghost subId_a_ghost subId_a subId_b	subId_ghost subIdBis_ghost subId_a_ghost1 subId_a_ghost2 subId_a_ghost3 subId_a1 subId_a2 subId_b1 subId_b2

• Layer 4 (Laws relying on Dedekind's law)

  	pdf	Statements	Test files	Proofs
  Definitions
  Verifications	layer4	xvi_a xvi_b_ghost xvi_b xxi_b_ghost xxi xxviii_a_ghost xxviii_a xxviii_b_ghost xxviii_b xxx_a xxx_b xxiii_a xxiii_b	xvi_a xvi_b_ghost xvi_b xxi_b_ghost xxi xxviii_a_ghost xxviii_a xxviii_b_ghost xxviii_b xxx_a xxx_b xxiii_a xxiii_b	xvi_a1 xvi_a2 xvi1 xvi_b_ghost xvi2 xxi_b_ghost1 xxi_b_ghost2 xxi_b_ghost3 xxi xxviii_a_ghost1 xxviii_a_ghost2 xxviii_a_ghost3 xxviii_a1 xxviii_a2 xxviii1 xxviii_b_ghost1 xxviii_b_ghost2 xxviii_b_ghost3 xxviii2 xxx1 xxx2 xxiii1 xxiii2

• Still pending

  	pdf	Statements	Test files	Proofs
  Definitions
  Verifications

Conference abstract

References