非表示:
キーワード:
-
要旨:
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, discussing the main design decisions
and features that influence Darwin's performance. We also report on practical
experiments carried out with problems from the CASC-J2 system competition and
parts of the TPTP Problem Library, and compare the results with those of other
state-of-the-art theorem provers.
