SourceForge has been redesigned. Learn more.
Close

[4b23aa]: / thys / PseudoHoops / document / root.tex  Maximize  Restore  History

Download this file

87 lines (63 with data), 2.9 kB

 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 \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
%\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
%\<triangleq>, \<yen>, \<lozenge>
%\usepackage[greek,english]{babel}
%option greek for \<euro>
%option english (default language) for \<guillemotleft>, \<guillemotright>
\usepackage[latin1]{inputenc}
%for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
%\<threesuperior>, \<threequarters>, \<degree>
\usepackage[only,bigsqcap]{stmaryrd}
%for \<Sqinter>
%\usepackage{eufrak}
%for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
%\usepackage{textcomp}
%for \<cent>, \<currency>
% 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: