Baumgartner, Peter; Fuchs, Alexander; Tinelli, Cesare
Darwin is the first implementation of the Model Evolution Calculus by Baumgartner and Tinelli. The Model Evolution Calculus lifts the DPLL procedure to first-order logic. Darwin is meant to be a fast and clean implementation of the calculus, showing its effectiveness and providing a base for further improvements and extensions. Based on a brief summary of the Model Evolution Calculus, we describe in the main part of the paper Darwin's proof procedure and its data structures and algorithms,...[Show more]
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.