Darwin is an automated theorem prover for first order clausal logic. It accepts problems formulated in tptp or tme format, non-clausal tptp problems are clausified using the eprover. Equality is not built into the currently implemented version of the calculus, it is instead automatically axiomatized for a given problem. Darwin is a decision procedure for function-free clause sets, and is in general faster and scales better on such problems than propositional approaches. Darwin is the first implementation of the Model Evolution Calculus (see papers below). The Model Evolution Calculus lifts the propositional DPLL procedure to first-order logic. One of the main motivations for this approach was the possibility of migrating to the first-order level some of those very effective search techniques developed by the SAT community for the DPLL procedure. The current version of Darwin implements first-order versions of unit propagation inference rules analogously to a restricted form of unit resolution and subsumption by unit clauses. To retain completeness, it includes a first-order version of the (binary) propositional splitting inference rule.

References in zbMATH (referenced in 13 articles )

Showing results 1 to 13 of 13.
Sorted by year (citations)

  1. de Nivelle, Hans: Theorem proving for classical logic with partial functions by reduction to Kleene logic (2017)
  2. Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: model representation (2016)
  3. Saghafi, Salman; Danas, Ryan; Dougherty, Daniel J.: Exploring theories with a model-finding assistant (2015)
  4. Baumgartner, Peter; Pelzer, Björn; Tinelli, Cesare: Model evolution with equality -- revised and implemented (2012)
  5. Gebser, Martin; Sabuncu, Orkunt; Schaub, Torsten: An incremental answer set programming based system for finite model computation (2011)
  6. Baumgartner, Peter; Thorstensen, Evgenij: Instance based methods - A brief overview (2010) ioport
  7. Piskac, Ruzica; de Moura, Leonardo; Bjørner, Nikolaj: Deciding effectively propositional logic using DPLL and substitution sets (2010)
  8. Baumgartner, Peter; Fuchs, Alexander; de Nivelle, Hans; Tinelli, Cesare: Computing finite models by reduction to function-free clause logic (2009)
  9. Baumgartner, Peter; Tinelli, Cesare: The model evolution calculus as a first-order DPLL method (2008)
  10. Udrea, Octavian; Lumezanu, Cristian; Foster, Jeffrey S.: Rule-based static analysis of network protocol implementations (2008)
  11. Fermüller, Christian G.; Pichler, Reinhard: Model representation over finite and infinite signatures (2007)
  12. Baumgartner, Peter; Fuchs, Alexander; Tinelli, Cesare: Lemma learning in the model evolution calculus (2006)
  13. Fermüller, Christian G.; Pichler, Reinhard: Model representation via contexts and implicit generalizations (2005)