mainBooleanAlgebrasIntro2 - Summary

 
 
Membership Info
Group Admin:
1 active member

Group identification
Id: 11312
System Name: bool2
Name: BooleanAlgebrasIntro2
Group Type: non-GNU software and documentation

Search in this Group


 

This group is not part of the GNU Project.

This development begins with basic utilities and math from Introduction to Boolean Algebras by Givant/Halmos on Springer.  After Sikorski's extension criterion and Kuratowski's monomorphism criterion, there are some attempts to code free algebras that withered after philosophical confusion regarding what code was most in demand. I toyed with function algebras a bit, with some definitions from Dietlinde Lau's Function Algebras on Springer. I never got to classical theorems.  Finally, I settled on Horst Reichel's monograph Structural Induction on Partial Algebras (the first edition title) that also goes by the second edition title Initial Computability, Algebraic Specificiations, Partial Algeras.  This monograph is quite phenomenal, and states in the forward that "The aim of this book is the initiation of an increasing use of partial algebras, especially in computer science." That's in demand enough!  Hopefully 40 years is enough for a full translation into Coq.

Registration Date: Tue 01 Jul 2014 03:09:01 AM UTC
License: GNU Lesser General Public License
Development Status: 3 - Alpha

 

Latest News rss feed
Ataboy
     posted by deluger, Mon 16 Jan 2023 04:13:59 AM UTC

I always feel uncomfortable without a background C development.
So, now that there's something too Sturm und Drang about a Boolean CAS, how about applied term algebras!
The good news is I have a simpler specification and interface (boyoboy); words (in a free semigroup) are easier to deal with than bits and whatnot (or at least the way [...]

Sneak Peak: Trees b y Serre
     posted by deluger, Mon 26 Dec 2022 10:44:49 PM UTC

And I still haven't forgot about finishing Term Algebras.  I'll need Jean Pierre Serre's "Trees" for that.  Am still learning it.

Back from the dead!
     posted by deluger, Fri 23 Dec 2022 06:40:21 AM UTC

Having given up on financial "day jobs" with C and Boolean Algebras (Atomizer), for the past many months or so, I've been working on my new long-term goal in Coq that will take many many years to get to -- exhibiting the free generators of the interval algebra on rational endpoints.  I had always wanted to get Topology back into the [...]

This project is semi-permanently retired
     posted by deluger, Mon 30 May 2022 04:07:09 PM UTC

My final consensus of Coq is that it's the most powerful language whose behavior no one can explain.  People often criticize math formalization for not doing enough.  I am officially stopping Coq development after 8 years because it does TOO MUCH. It was the main work that flipped a bit in the Great Spirit and made me happy with honey! Now [...]

Quick Overview
 Memberlist (1 member)

Communication Tools
 Mailing Lists (0 public mailing lists)

Development Tools
 Task Manager (open items: 0, total: 0)

Back to the top

Powered by Savane 3.13-3230.
Corresponding source code