Email Gateway (Aug 22 2022 at 14:04): Email Gateway (Aug 22 2022 at 14:04):From: Tobias Nipkow <nipkow@in.tum.de>
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!
smime.p7s
Last updated: Nov 04 2025 at 08:30 UTC