We derive rewrite-based ordered resolution calculi for semi-lattices, distributive lattices and boolean lattices. Using ordered resolution as a metaprocedure, theory axioms are first transformed into independent bases. Focused inference rules are then extracted from inference patterns in refutations. The derivation is guided by mathematical and procedural background knowledge, in particular by ordered chaining calculi for quasiorderings (forgetting the lattice structure), by ordered resolution (forgetting the clause structure) and by Knuth-Bendix completion for non-symmetric transitive relations (forgetting both structures). Conversely, all three calculi are derived and proven complete in a transparent and generic way as special cases of the lattice calculi.
展开▼
