Superposition and Model Evolution Combined

Date

Authors

Baumgartner, Peter

Waldmann, Uwe

Publisher

Springer

Abstract

We present a new calculus for first-order theorem proving with equality, Με+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-tri

Keywords

Keywords: DPLL procedure; First-order; Inference rules; Model evolution; Model evolution calculus; Non-trivial; Simplification rules; Superposition calculus; Automation; Biomineralization; Quality assurance; Redundancy; Theorem proving; Calculations

URI

http://hdl.handle.net/1885/57194

Collections

ANU Research Publications

Source

Proceedings of the 22nd International Conference on Automated Deduction

Type

Conference paper

DOI

10.1007/978-3-642-02959-2_2

Restricted until

2037-12-31

Downloads

File

Description

01_Baumgartner_Superposition_and_Model_2009.pdf (273.74 KB)