| Projects on Google Code | Results 1 - 5 of 5 |
= The Flyspeck Project =
== Introduction ==
The purpose of the flyspeck project is to produce a formal proof
of the Kepler Conjecture. The name `flyspeck' comes from matching the pattern {{{/f.*p.*k/}}}
against an English dictionary. FPK in turn is an acronym for "The Formal Proof
o...
This suite of tools consists of:
* hylores : a resolution-based theorem prover for the hybrid logic H(@,A,D,◇¯,↓)
* htab : a tableaux-based theorem prover for the hybrid logic H(@,A,D,◇¯,↓) with role inclusion
* hylolib : the common library used by the other provers
* gridtest : a framewor...
TheoremProving,
logic,
ModalLogic,
proof,
haskell,
HybridLogic,
resolution,
tableaux,
tableau,
descriptionlogic
= ACL2 Books Development =
This site is for community-driven development for the basic ACL2 libraries, which deal with topics like arithmetic, data structures, and hardware modelling. We're working with the authors of ACL2 and our changes are eventually incorporated into official ACL2 releases.
...
We attempt to prove the famous theorem of Galois of
abstract algebra giving the relationship between
fixed fields of certain field isomorphisms and subgroups
of the Galois group of such isomorphisms.
copy from file... todo