Theorem prover input files

From Structures

Jump to: navigation, search

Here is a list of strucures for which there is an axiomatization that is suitable as input for a theorem prover. The current format is based on the one used by Prover9/Mace4, but converters to other formats (e.g. the intermediate TPTP format) are planned.

Here is a template (ascii) for starting a new class below.

[edit]

Alphabetical list of structures with first-order axioms (ascii)

  1. Abelian groups (ascii)
  2. Abelian lattice-ordered groups (ascii)
  3. Abelian ordered groups (ascii)
  4. Abelian p-groups (ascii)
  5. Abelian partially ordered groups (ascii)
  6. Action algebras (ascii)
  7. Action lattices (ascii)
  8. Allegories (ascii)
  9. Almost distributive lattices (ascii)
  10. Bands (ascii)
  11. Basic logic algebras (ascii)
  12. BCI-algebras (ascii)
  13. BCK-algebras (ascii)
  14. BCK-join-semilattices (ascii)
  15. BCK-lattices (ascii)
  16. BCK-meet-semilattices (ascii)
  17. BL-algebras (ascii)
  18. Boolean algebras (ascii)
  19. Boolean groups (ascii)
  20. Boolean lattices (ascii)
  21. Boolean monoids (ascii)
  22. Boolean rings (ascii)
  23. Boolean semigroups (ascii)
  24. Boolean semilattices (ascii)
  25. Bounded distributive lattices (ascii)
  26. Bounded lattices (ascii)
  27. Bounded residuated lattices (ascii)
  28. Brouwerian algebras (ascii)
  29. Brouwerian semilattices (ascii)
  30. Cancellative commutative monoids (ascii)
  31. Cancellative commutative semigroups (ascii)
  32. Cancellative monoids (ascii)
  33. Cancellative semigroups (ascii)
  34. Cancellative residuated lattices (ascii)
  35. Categories (ascii)
  36. Chains (ascii)
  37. Clifford semigroups (ascii)
  38. Closure algebras (ascii)
  39. Commutative BCK-algebras (ascii)
  40. Commutative groupoids (ascii)
  41. Commutative inverse semigroups (ascii)
  42. Commutative lattice-ordered monoids (ascii)
  43. Commutative lattice-ordered rings (ascii)
  44. Commutative lattice-ordered semigroups (ascii)
  45. Commutative monoids (ascii)
  46. Commutative ordered monoids (ascii)
  47. Commutative ordered rings (ascii)
  48. Commutative ordered semigroups (ascii)
  49. Commutative partially ordered monoids (ascii)
  50. Commutative partially ordered semigroups (ascii)
  51. Commutative regular rings (ascii)
  52. Commutative residuated lattice-ordered semigroups (ascii)
  53. Commutative residuated lattices (ascii)
  54. Commutative residuated partially ordered monoids (ascii)
  55. Commutative residuated partially ordered semigroups (ascii)
  56. Commutative rings (ascii)
  57. Commutative rings with identity (ascii)
  58. Commutative semigroups (ascii)
  59. Complemented lattices (ascii)
  60. Complemented distributive lattices (ascii)
  61. Complemented modular lattices (ascii)
  62. Completely regular semigroups (ascii)
  63. Cylindric algebras (ascii)
  64. De Morgan algebras (ascii)
  65. De Morgan monoids (ascii)
  66. Dedekind categories (ascii)
  67. Dense linear orders (ascii)
  68. Digraph algebras (ascii)
  69. Directed partial orders (ascii)
  70. Directed graphs (ascii)
  71. Directoids (ascii)
  72. Distributive allegories (ascii)
  73. Distributive double p-algebras (ascii)
  74. Distributive dual p-algebras (ascii)
  75. Distributive lattices (ascii)
  76. Distributive lattice ordered semigroups (ascii)
  77. Distributive p-algebras (ascii)
  78. Distributive residuated lattices (ascii)
  79. Division rings (ascii)
  80. Double Stone algebras (ascii)
  81. Dunn monoids (ascii)
  82. Dynamic algebras (ascii)
  83. Entropic groupoids (ascii)
  84. Equivalence algebras (ascii)
  85. Equivalence relations (ascii)
  86. f-rings (ascii)
  87. Fields (ascii)
  88. FL-algebras (ascii)
  89. FLc-algebras (ascii)
  90. FLe-algebras (ascii)
  91. FLew-algebras (ascii)
  92. FLw-algebras (ascii)
  93. Function rings (ascii)
  94. Generalized BL-algebras (ascii)
  95. Generalized Boolean algebras (ascii)
  96. Generalized MV-algebras (ascii)
  97. Goedel algebras (ascii)
  98. Graphs (ascii)
  99. Groupoids (ascii)
  100. Groups (ascii)
  101. Heyting algebras (ascii)
  102. Hilbert algebras (ascii)
  103. Hoops (ascii)
  104. Idempotent semirings (ascii)
  105. Idempotent semirings with domain (ascii)
  106. Idempotent semirings with identity (ascii)
  107. Idempotent semirings with identity and zero (ascii)
  108. Idempotent semirings with zero (ascii)
  109. Implication algebras (ascii)
  110. Implicative lattices (ascii)
  111. Integral domains (ascii)
  112. Integral ordered monoids (ascii)
  113. Integral relation algebras (ascii)
  114. Integral residuated lattices (ascii)
  115. Intuitionistic linear logic algebras (ascii)
  116. Inverse semigroups (ascii)
  117. Involutive lattices (ascii)
  118. Involutive residuated lattices (ascii)
  119. Join-semidistributive lattices (ascii)
  120. Join-semilattices (ascii)
  121. Jordan algebras (ascii)
  122. Kleene algebras (ascii)
  123. Kleene lattices (ascii)
  124. Lambek algebras (ascii)
  125. Lattice-ordered groups (ascii)
  126. Lattice-ordered monoids (ascii)
  127. Lattice-ordered rings (ascii)
  128. Lattice-ordered semigroups (ascii)
  129. Lattices (ascii)
  130. Left cancellative semigroups (ascii)
  131. Lie algebras (ascii)
  132. Linear Heyting algebras (ascii)
  133. Linear logic algebras (ascii)
  134. Linear orders (ascii)
  135. Loops (ascii)
  136. Medial groupoids (ascii)
  137. Medial quasigroups (ascii)
  138. Meet-semidistributive lattices (ascii)
  139. Meet-semilattices (ascii)
  140. Modal algebras (ascii)
  141. Modular lattices (ascii)
  142. Modular ortholattices (ascii)
  143. Monadic algebras (ascii)
  144. Monoidal t-norm logic algebras (ascii)
  145. Monoids (ascii)
  146. Moufang loops (ascii)
  147. Moufang quasigroups (ascii)
  148. Multiplicative additive linear logic algebras (ascii)
  149. Multiplicative lattices (ascii)
  150. Multiplicative semilattices (ascii)
  151. MV-algebras (ascii)
  152. Neardistributive lattices (ascii)
  153. Near-rings (ascii)
  154. Near-rings with identity (ascii)
  155. Near-fields (ascii)
  156. Nilpotent groups (ascii)
  157. Nonassociative relation algebras (ascii)
  158. Normal bands (ascii)
  159. Ockham algebras (ascii)
  160. Order algebras (ascii)
  161. Ordered fields (ascii)
  162. Ordered groups (ascii)
  163. Ordered monoids (ascii)
  164. Ordered monoids with zero (ascii)
  165. Ordered rings (ascii)
  166. Ordered semigroups (ascii)
  167. Ordered sets (ascii)
  168. Ortholattices (ascii)
  169. Orthomodular lattices (ascii)
  170. Partial groupoids (ascii)
  171. Partially ordered groups (ascii)
  172. Partially ordered monoids (ascii)
  173. Partially ordered semigroups (ascii)
  174. Partially ordered sets (ascii)
  175. Peirce algebras (ascii)
  176. Pocrims (ascii)
  177. Pointed residuated lattices (ascii)
  178. Polrims (ascii)
  179. Polyadic algebras (ascii)
  180. Posets (ascii)
  181. Post algebras (ascii)
  182. Preordered sets (ascii)
  183. Process algebras (ascii)
  184. Pseudo basic logic algebras (ascii)
  185. Pseudo MTL-algebras (ascii)
  186. Pseudo MV-algebras (ascii)
  187. Pseudocomplemented distributive lattices (ascii)
  188. Pure discriminator algebras (ascii)
  189. Quasigroups (ascii)
  190. Quasi-implication algebras (ascii)
  191. Quasi-ordered sets (ascii)
  192. Quasitrivial groupoids (ascii)
  193. Rectangular bands (ascii)
  194. Reflexive relations (ascii)
  195. Regular rings (ascii)
  196. Regular semigroups (ascii)
  197. Relation algebras (ascii)
  198. Relative Stone algebras (ascii)
  199. Relativized relation algebras (ascii)
  200. Representable cylindric algebras (ascii)
  201. Representable lattice-ordered groups (ascii)
  202. Representable relation algebras (ascii)
  203. Representable residuated lattices (ascii)
  204. Residuated idempotent semirings (ascii)
  205. Residuated lattice-ordered semigroups (ascii)
  206. Residuated lattices (ascii)
  207. Residuated partially ordered monoids (ascii)
  208. Residuated partially ordered semigroups (ascii)
  209. Rings (ascii)
  210. Rings with identity (ascii)
  211. Schroeder categories (ascii)
  212. Semiassociative relation algebras (ascii)
  213. Semidistributive lattices (ascii)
  214. Semigroups (ascii)
  215. Semigroups with identity (ascii)
  216. Semigroups with zero (ascii)
  217. Semilattices (ascii)
  218. Semilattices with identity (ascii)
  219. Semilattices with zero (ascii)
  220. Semirings (ascii)
  221. Semirings with identity (ascii)
  222. Semirings with identity and zero (ascii)
  223. Semirings with zero (ascii)
  224. Sequential algebras (ascii)
  225. Shells (ascii)
  226. Skew-fields (ascii)
  227. Small categories (ascii)
  228. Steiner quasigroups (ascii)
  229. Stone algebras (ascii)
  230. Symmetric relations (ascii)
  231. Tarski algebras (ascii)
  232. Tense algebras (ascii)
  233. Temporal algebras (ascii)
  234. Totally ordered monoids (ascii)
  235. Transitive relations (ascii)
  236. Trees (ascii)
  237. Tournaments (ascii)
  238. Unary algebras (ascii)
  239. Unital rings (ascii)
  240. Wajsberg algebras (ascii)
  241. Wajsberg hoops (ascii)
  242. Weakly associative lattices (ascii)
  243. Weakly associative relation algebras (ascii)
  244. Weakly representable relation algebras (ascii)
Retrieved from "http://math.chapman.edu/structures/index.php/Theorem_prover_input_files"
Personal tools