# [isabelle] New AFP entries: Superposition Calculus and Stone Algebras

*To*: Isabelle Users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] New AFP entries: Superposition Calculus and Stone Algebras
*From*: Tobias Nipkow <nipkow at in.tum.de>
*Date*: Tue, 6 Sep 2016 09:54:38 +0200
*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:45.0) Gecko/20100101 Thunderbird/45.3.0

More on logic and algebra:
A Variant of the Superposition Calculus
Nicolas Peltier

`We provide a formalization of a variant of the superposition calculus, together
``with formal proofs of soundness and refutational completeness (w.r.t. the usual
``redundancy criteria based on clause ordering). This version of the calculus uses
``all the standard restrictions of the superposition rules, together with the
``following refinement, inspired by the basic superposition calculus: each clause
``is associated with a set of terms which are assumed to be in normal form -- thus
``any application of the replacement rule on these terms is blocked. The set is
``initially empty and terms may be added or removed at each inference step. The
``set of terms that are assumed to be in normal form includes any term introduced
``by previous unifiers as well as any term occurring in the parent clauses at a
``position that is smaller (according to some given ordering on positions) than a
``previously replaced term. The standard superposition calculus corresponds to the
``case where the set of irreducible terms is always empty.
`
https://www.isa-afp.org/entries/SuperCalc.shtml
Stone Algebras
Walter Guttmann

`A range of algebras between lattices and Boolean algebras generalise the notion
``of a complement. We develop a hierarchy of these pseudo-complemented algebras
``that includes Stone algebras. Independently of this theory we study filters
``based on partial orders. Both theories are combined to prove Chen and GrÃtzer's
``construction theorem for Stone algebras. The latter involves extensive reasoning
``about algebraic structures in addition to reasoning in algebraic structures.
`
https://www.isa-afp.org/entries/Stone_Algebras.shtml
Enjoy!

**Attachment:
**`smime.p7s`

*Description:* S/MIME Cryptographic Signature

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*