1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 \documentclass[11pt,a4paper]{article} \usepackage{isabelle,isabellesym} % further packages required for unusual symbols (see also % isabellesym.sty), use only when needed %\usepackage{amssymb} %for \, \, \, \, \, \, %\, \, \, \, \, %\, \, \ %\usepackage[greek,english]{babel} %option greek for \ %option english (default language) for \, \ \usepackage[latin1]{inputenc} %for \, \, \, \, %\, \, \ \usepackage[only,bigsqcap]{stmaryrd} %for \ %\usepackage{eufrak} %for \ ... \, \ ... \ (also included in amssymb) %\usepackage{textcomp} %for \, \ % this should be the last package used \usepackage{pdfsetup} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} \begin{document} \title{Pseudo-hoops} \author{George Georgescu and Lauren\c tiu Leu\c stean and Viorel Preoteasa} \maketitle \begin{abstract} Pseudo-hoops are algebraic structures introduced in \cite{bosbach:1969,bosbach:1970} by B. Bosbach under the name of complementary semigroups. This is a formalization of the paper \cite{georgescu:leustean:preoteasa:2005}. Following \cite{georgescu:leustean:preoteasa:2005} we prove some properties of pseudo-hoops and we define the basic concepts of filter and normal filter. The lattice of normal filters is isomorphic with the lattice of congruences of a pseudo-hoop. We also study some important classes of pseudo-hoops. Bounded Wajsberg pseudo-hoops are equivalent to pseudo-Wajsberg algebras and bounded basic pseudo-hoops are equiv- alent to pseudo-BL algebras. Some examples of pseudo-hoops are given in the last section of the formalization. \end{abstract} \tableofcontents \section{Overview} Section 2 introduces some operations and their infix syntax. Section 3 and 4 introduces some facts about residuated and complemented monoids. Section 5 introduces the pseudo-hoops and some of their properties. Section 6 introduces filters and normal filters and proves that the lattice of normal filters and the lattice of congruences are isomorphic. Following \cite{ceterchi:2001}, section 7 introduces pseudo-Waisberg algebras and some of their properties. In Section 8 we investigate some classes of pseudo-hoops. Finally section 9 presents some examples of pseudo-hoops and normal filters. \parindent 0pt\parskip 0.5ex % generated text of all theories \input{session} % optional bibliography \bibliographystyle{abbrv} \bibliography{root} \end{document} %%% Local Variables: %%% mode: latex %%% TeX-master: t %%% End: