------------------------------------------------------------------------------- Axioms 1212 sets (155 abstract, 131 CNF, 1042 FOF, 8 TFF, 39 THF) ------------------------------------------------------------------------------- AGT001 ( -0 +3 _0 ^0) CPlanT system ALG001 ( -1 +0 _0 ^0) Abstract algebra axioms, based on Godel set theory ALG002 ( -0 +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 _0 ^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 _2 ^0) Integer collections 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 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 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 ^1) 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. MSC001 ( -3 +0 _0 ^0) Sets, numbers, lists, etc, that make up the Isabelle/HOL library 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 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 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 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 TOP001 ( -1 +0 _0 ^0) Point-set topology