English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
  Local TagsRelease HistoryDetailsSummary

Released
Journal Article

Implementing the Model Evolution Calculus

MPS-Authors
/persons/resource/persons44088

Baumgartner,  Peter
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons44452

Fuchs,  Alexander
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available
Citation

Baumgartner, P., Fuchs, A., & Tinelli, C. (2006). Implementing the Model Evolution Calculus. International Journal on Artificial Intelligence Tools, 15, 21-52.


Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-2322-6
Abstract
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.