Baumgartner, PeterWaldmann, Uwe2015-12-100168-7433http://hdl.handle.net/1885/58990We present a new calculus for first-order theorem proving with equality, Mσ+Sup, which generalizes both the Superposition calculus and the Model Evolution calculus (with equality) by integrating their inference rules and redundancy criteria in a non-trivKeywords: DPLL procedure; Equality; First-order; Inference rules; Instance-based methods; Model evolution; Model evolution calculus; Model representation; Non-trivial; Simplification rules; Superposition; Superposition calculus; Biomineralization; Redundancy; Theor Equality; Instance based methods; Model evolution; Superposition201010.1007/s10817-010-9214-x2016-02-24