-------------------------------------------------------------------------------- Axioms 1976 sets (314 abstract, 133 CNF, 1354 FOF, 461 TFF, 489 THF) -------------------------------------------------------------------------------- AGT001 ( -0 +3 _0 ^0) CPlanT system ALG001 ( -1 +0 _0 ^0) Abstract algebra axioms, based on Godel set theory ALG002 ( -1 +1 _0 ^0) Median algebra axioms ALG003 ( -0 +0 _0 ^1) Untyped lambda sigma calculus ANA001 ( -1 +0 _0 ^0) Analysis (limits) axioms for continuous functions ANA002 ( -1 +0 _0 ^0) Analysis (limits) axioms for continuous functions ANA003 ( -1 +0 _0 ^0) A theory of Big-O notation BIO001 ( -0 +1 _0 ^0) Textbook biology BOO001 ( -1 +0 _0 ^0) Ternary Boolean algebra (equality) axioms BOO002 ( -1 +0 _0 ^0) Boolean algebra axioms BOO003 ( -1 +0 _0 ^0) Boolean algebra (equality) axioms BOO004 ( -1 +0 _0 ^0) Boolean algebra (equality) axioms CAT001 ( -1 +0 _0 ^0) Category theory axioms CAT002 ( -1 +0 _0 ^0) Category theory (equality) axioms CAT003 ( -1 +0 _0 ^0) Category theory axioms CAT004 ( -1 +0 _0 ^0) Category theory axioms COL001 ( -1 +0 _0 ^0) Type-respecting combinators COL002 ( -2 +0 _0 ^0) Combinators COM001 ( -0 +2 _0 ^0) Common axioms for progress/preservation proof CSR001 ( -0 +4 _2 ^0) Standard discrete event calculus axioms CSR002 ( -0 +6 _0 ^0) 0 axioms from Cyc CSR003 ( -0 +6 _0 ^0) SUMO CSR004 ( -0 +1 _0 ^0) LogAnswer CSR005 ( -0 +0 _0 ^1) SUMO CSR006 ( -0 +1 _0 ^0) Adimen SUMO DAT001 ( -0 +0 _1 ^0) Integer arrays DAT002 ( -0 +0 _1 ^0) Integer collections with counting DAT003 ( -0 +0 _1 ^0) Pointer data types DAT004 ( -0 +0 _1 ^0) Array data types DAT005 ( -0 +0 _1 ^0) Heap data types DAT006 ( -0 +0 _1 ^0) Tree-heap data types FLD001 ( -1 +0 _0 ^0) Ordered field axioms (axiom formulation glxx) FLD002 ( -1 +0 _0 ^0) Ordered field axioms (axiom formulation re) GEO001 ( -2 +0 _0 ^0) Tarski geometry axioms GEO002 ( -4 +0 _0 ^0) Tarski geometry axioms GEO003 ( -1 +0 _0 ^0) Hilbert geometry axioms GEO004 ( -4 +4 _0 ^0) Simple curve axioms GEO005 ( -1 +0 _0 ^0) Hilbert geometry axioms, adapted to respect multi-sortedness GEO006 ( -0 +7 _0 ^0) Apartness geometry GEO007 ( -0 +2 _0 ^0) Ordered affine geometry GEO008 ( -0 +1 _0 ^0) Apartness geometry GEO009 ( -0 +1 _0 ^0) Ordered affine geometry with definitions GEO010 ( -0 +2 _0 ^0) Flyspeck project GEO011 ( -0 +1 _0 ^0) Tarskian geometry GEO012 ( -0 +1 _0 ^0) Deductive Databases Method in Geometry GRA001 ( -0 +1 _0 ^0) Directed graphs and paths GRP001 ( -1 +0 _0 ^0) Monoid axioms GRP002 ( -1 +0 _0 ^0) Semigroup axioms GRP003 ( -3 +1 _0 ^0) Group theory axioms GRP004 ( -3 +1 _0 ^0) Group theory (equality) axioms GRP005 ( -1 +0 _0 ^0) Group theory axioms GRP006 ( -1 +0 _0 ^0) Group theory (Named groups) axioms GRP007 ( -0 +1 _0 ^0) Group theory (Named Semigroups) axioms GRP008 ( -2 +0 _0 ^0) Semigroups axioms HAL001 ( -0 +1 _0 ^0) Standard homological algebra axioms HEN001 ( -1 +0 _0 ^0) Henkin model axioms HEN002 ( -1 +0 _0 ^0) Henkin model axioms HEN003 ( -1 +0 _0 ^0) Henkin model (equality) axioms HWC001 ( -1 +0 _0 ^0) Definitions of AND, OR and NOT HWC002 ( -1 +0 _0 ^0) Definitions of AND, OR and NOT HWV001 ( -3 +0 _0 ^0) Connections, faults, and gates. HWV002 ( -3 +0 _0 ^0) Connections, faults, and gates. HWV003 ( -1 +0 _0 ^0) Axioms from a VHDL design description HWV004 ( -1 +0 _0 ^0) Axioms from a VHDL design description ITP001 ( -0 +1 _1 ^1) HOL4 set theory export, bushy and chainy mode ITP002 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP003 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP004 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP005 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP006 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP007 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP008 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP009 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP010 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP011 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP012 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP013 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP014 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP015 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP016 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP017 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP018 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP019 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP020 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP021 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP022 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP023 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP024 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP025 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP026 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP027 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP028 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP029 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP030 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP031 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP032 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP033 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP034 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP035 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP036 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP037 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP038 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP039 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP040 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP041 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP042 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP043 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP044 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP045 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP046 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP047 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP048 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP049 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP050 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP051 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP052 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP053 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP054 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP055 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP056 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP057 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP058 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP059 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP060 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP061 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP062 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP063 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP064 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP065 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP066 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP067 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP068 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP069 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP070 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP071 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP072 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP073 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP074 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP075 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP076 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP077 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP078 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP079 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP080 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP081 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP082 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP083 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP084 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP085 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP086 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP087 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP088 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP089 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP090 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP091 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP092 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP093 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP094 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP095 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP096 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP097 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP098 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP099 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP100 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP101 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP102 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP103 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP104 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP105 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP106 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP107 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP108 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP109 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP110 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP111 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP112 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP113 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP114 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP115 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP116 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP117 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP118 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP119 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP120 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP121 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP122 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP123 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP124 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP125 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP126 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP127 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP128 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP129 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP130 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP131 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP132 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP133 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP134 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP135 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP136 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP137 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP138 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP139 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP140 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP141 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP142 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP143 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP144 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP145 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP146 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP147 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP148 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP149 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP150 ( -0 +2 _3 ^3) HOL4 syntactic export, chainy mode ITP002 ( -0 +0 _0 ^1) ROCQ axioms KLE001 ( -0 +8 _0 ^0) Idempotent semirings KLE002 ( -0 +1 _0 ^0) Kleene algebra KLE003 ( -0 +1 _0 ^0) Omega algebra KLE004 ( -0 +1 _0 ^0) Demonic Refinement Algebra KRS001 ( -0 +2 _0 ^0) SZS success ontology nodes LAT001 ( -5 +0 _0 ^0) Lattice theory (equality) axioms LAT002 ( -1 +0 _0 ^0) Lattice theory axioms LAT003 ( -1 +0 _0 ^0) Ortholattice theory (equality) axioms LAT004 ( -1 +0 _0 ^0) Quasilattice theory (equality) axioms LAT005 ( -1 +0 _0 ^0) Weakly Associative Lattices theory (equality) axioms LAT006 ( -3 +0 _0 ^0) Tarski's fixed point theorem (equality) axioms LCL001 ( -3 +0 _0 ^0) Wajsberg algebra LCL002 ( -2 +0 _0 ^0) Alternative Wajsberg algebra LCL003 ( -1 +0 _0 ^0) Propositional logic deduction LCL004 ( -3 +0 _0 ^0) Propositional logic deduction LCL005 ( -1 +0 _0 ^0) Propositional logic LCL006 ( -0 +6 _0 ^0) Propositional logic rules and axioms LCL007 ( -0 +7 _0 ^0) Propositional modal logic rules and axioms LCL008 ( -0 +0 _0 ^1) Multi-Modal Logic LCL009 ( -0 +0 _0 ^1) Translating constructive S4 (CS4) to bimodal classical S4 (BS4) LCL010 ( -0 +0 _0 ^1) Propositional intuitionistic logic in HOL LCL011 ( -0 +0 _0 ^1) Propositional intuitionistic logic in HOL LCL012 ( -0 +0 _0 ^1) Propositional intuitionistic logic in HOL LCL013 ( -0 +0 _0 ^7) Embedding of quantified multimodal logic in simple type theory LCL014 ( -0 +0 _0 ^1) Region Connection Calculus LCL015 ( -0 +0 _0 ^2) Embedding of quantified multimodal logic in simple type theory LCL016 ( -0 +0 _0 ^2) Embedding of second order modal logic in simple type theory LCL017 ( -0 +0 _0 ^2) Embedding of second order modal logic S5 with universal access LDA001 ( -1 +0 _0 ^0) Embedding algebra MAT001 ( -0 +0 _0 ^1) Untyped lambda sigma calculus MED001 ( -0 +2 _0 ^0) Physiology Diabetes Mellitus type 2 MED002 ( -0 +1 _0 ^0) Medical subject headings MGT001 ( -1 +1 _0 ^0) Inequalities. MGT002 ( -0 +9 _0 ^0) Strict total order for interval reasoning MSC001 ( -3 +0 _0 ^0) Sets, numbers, lists, etc, that make up the Isabelle/HOL library MVA001 ( -1 +0 _0 ^0) Generalized MV algebras (equality) NLP001 ( -0 +1 _0 ^0) Wordnet NUM001 ( -3 +0 _0 ^0) Number theory axioms NUM002 ( -1 +0 _0 ^0) Number theory (equality) axioms NUM003 ( -1 +0 _0 ^0) Number theory axioms, based on Godel set theory NUM004 ( -1 +0 _0 ^0) Number theory (ordinals) axioms, based on NBG set theory NUM005 ( -0 +3 _0 ^0) Translating from nXXX to rdn notation NUM006 ( -0 +0 _0 ^1) Church Numerals in Simple Type Theory NUM007 ( -0 +0 _0 ^5) Grundlagen preliminaries NUM008 ( -0 +1 _0 ^0) Robinson arithmetic with equality NUM009 ( -0 +1 _0 ^0) Robinson arithmetic without equality PHI001 ( -0 +0 _0 ^1) Axioms for Goedel's Ontological Proof of the Existence of God PHI002 ( -0 +2 _0 ^0) Definitions for Spinoza's Ethics - the DAPI PLA001 ( -2 +0 _0 ^0) Blocks world axioms PLA002 ( -0 +1 _0 ^0) Blocks world axioms PRD001 ( -0 +1 _0 ^0) Wine facts PUZ001 ( -1 +0 _0 ^0) Mars and Venus axioms PUZ002 ( -1 +0 _0 ^0) Truthtellers and Liars axioms for two types of people PUZ003 ( -1 +0 _0 ^0) Truthtellers and Liars axioms for three types of people PUZ004 ( -1 +0 _0 ^0) Quo vadis axioms PUZ005 ( -1 +1 _0 ^0) Sudoku axioms PUZ006 ( -0 +1 _0 ^0) Sudoku axioms QUA001 ( -0 +0 _0 ^2) Quantales REL001 ( -2 +2 _0 ^0) Relation Algebra RNG001 ( -1 +0 _0 ^0) Ring theory axioms RNG002 ( -1 +0 _0 ^0) Ring theory (equality) axioms RNG003 ( -1 +0 _0 ^0) Alternative ring theory (equality) axioms RNG004 ( -1 +0 _0 ^0) Alternative ring theory (equality) axioms RNG005 ( -1 +0 _0 ^0) Ring theory (equality) axioms ROB001 ( -2 +0 _0 ^0) Robbins algebra axioms SET001 ( -4 +0 _0 ^0) Membership and subsets SET002 ( -1 +0 _0 ^0) Set theory axioms SET003 ( -1 +0 _0 ^0) Set theory axioms based on Godel set theory SET004 ( -2 +0 _0 ^0) Set theory axioms based on NBG set theory SET005 ( -0 +1 _0 ^0) Set theory axioms based on NBG set theory SET006 ( -0 +5 _0 ^0) Naive set theory based on Goedel's set theory SET007 ( -0+930 _0 ^0) Mizar Built-in Notions SET008 ( -0 +0 _0 ^3) Basic set theory definitions SET009 ( -0 +0 _0 ^1) Binary relations SET010 ( -0 +1 _0 ^0) Hereditary finite sets SWB001 ( -0 +1 _0 ^0) OWL 2 Full SWB002 ( -0 +1 _0 ^0) ALCO Full Extensional SWB003 ( -0 +2 _0 ^0) RDFS SWC001 ( -1 +1 _0 ^0) List specification SWV001 ( -1 +0 _0 ^0) Program verification axioms SWV002 ( -1 +0 _0 ^0) Program verification axioms SWV003 ( -0 +1 _0 ^0) NASA software certification axioms SWV004 ( -1 +0 _0 ^0) Cryptographic protocol axioms for messages SWV005 ( -8 +0 _0 ^0) Cryptographic protocol axioms for messages SWV006 ( -4 +0 _0 ^0) Cryptographic protocol axioms for public SWV007 ( -0 +5 _0 ^0) Priority queue checker: quasi-order set with bottom element SWV008 ( -0 +0 _0 ^3) ICL logic based upon modal logic based upon simple type theory SWV009 ( -0 +1 _0 ^0) General axioms for access to classified information SWV010 ( -0 +0 _0 ^1) Translation from Binder Logic (BL) to CS4 SWV011 ( -0 +1 _0 ^0) Axioms for verification of Stoller's leader election algorithm SWV012 ( -0 +1 _0 ^0) Syntactic definitions of the logical operators SWV013 ( -1 +0 _0 ^0) Lists in Separation Logic SWV014 ( -0 +0 _1 ^0) Anthem standard preamble SYN000 ( -1 +1 _1 ^1) A simple include file for FOF SYN001 ( -1 +0 _0 ^0) Synthetic domain theory for EBL SYN002 ( -0 +1 _0 ^0) Orevkov formula TIM001 ( -0 +0 _1 ^0) Stanica computation axioms TIM002 ( -0 +0 _2 ^0) Allens axioms for interval algebra TOP001 ( -1 +0 _0 ^0) Point-set topology