[4b23aa]: / web / entries / PseudoHoops.shtml  Maximize  Restore  History

Download this file

96 lines (78 with data), 3.2 kB

<!DOCTYPE public "-//w3c//dtd html 4.01 transitional//en"
		"http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
  <title>Archive of Formal Proofs</title>
  <link rel="stylesheet" type="text/css" href="front.css">
  <link rel="icon" href="../images/favicon.ico" type="image/icon">
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
</head>
<body>

<table width="100%">
  <tbody>
    <tr>
      <td width="20%" align="center" valign="top">
      <!-- navigation -->
      <!--#include file="nav.html"-->
      </td>
      <td width="80%" valign="top">
      <!-- content -->

<div align="center">
<p> </p>

<h1><font class="first">P</font>seudo
<font class="first">H</font>oops
</h1>
<p></p>
<table width="80%" class="data">
  <tbody>
    <tr><td class="datahead" width="20%">Title:</td>
        <td class="data" width="80%">Pseudo Hoops</td></tr>

    <tr><td class="datahead">Author:</td>
        <td class="data">George Georgescu, Laurentiu Leustean and  <a href="http://users.abo.fi/vpreotea/">Viorel Preoteasa</a></td></tr>

    <tr><td class="datahead">Submission date:</td>
        <td class="data">2011-09-22</td></tr>

    <tr><td class="datahead" valign="top">Abstract:</td>
        <td class="abstract">

Pseudo-hoops are algebraic structures introduced by B. Bosbach under the name of complementary semigroups. In this formalization 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 equivalent to pseudo-BL algebras. Some examples of pseudo-hoops are given in the last section of the formalization.
        </td></tr>

    <tr><td class="datahead">License:</td>
        <td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>


<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
<!---INCLUDE- file="devel-warning.shtml"-->

  </tbody>
</table>

<p></p>

<!--#set var="name" value="PseudoHoops" -->
<!--#set var="binfo" value="../browser_info/current/HOL/LatticeProperties/${name}" -->

<!--#set var="doc" value="${binfo}/document.pdf" -->
<!--#set var="outline" value="${binfo}/outline.pdf" -->
<!--#set var="browse" value="${binfo}/index.html" -->
<!--#set var="tar" value="../release/afp-${name}-current.tar.gz" -->

<table class="links">
  <tbody>
    <tr>
  <td class="links">
	<a href="<!--#echo var="outline" -->">Proof outline</a><br>
	<a href="<!--#echo var="doc" -->">Proof document</a>
  </td>
	<!-- link to README.hmtl if no document exists -->	
	</tr>
    <tr>
  <td class="links">
	<a href="<!--#echo var="browse" -->">Browse theories</a>
	</td></tr>
    <tr>
  <td class="links"> 
	<a href="<!--#echo var="tar" -->">Download this entry</a>
	</td>
  </tr>
    <tr><td class="links">Older releases:
None    </td></tr>
  </tbody>
</table>
<!-- entry data end -->

</td> </tr> </table>

</body>
</html>