E-Darvin
E-Darwin is an automated theorem prover for first-order clausal logic with equality. It accepts problems in tptp or tme syntax. Non-clausal input is clausified using the eprover (or soon a built-in clausifier). E-Darwin implements the Model Evolution calculus and several variants thereof which include equality reasoning, see the papers. The system is a based on the Darwin prover. As Darwin is no longer actively maintained, E-Darwin will eventually subsume all of its functions. The development of E-Darwin forked off from Darwin 1.3, so at the moment E-Darwin still needs to catch up on the changes made between Darwin 1.3 and its last version, Darwin 1.4.5.
Keywords for this software
References in zbMATH (referenced in 16 articles , 1 standard article )
Showing results 1 to 16 of 16.
Sorted by year (- de Nivelle, Hans: Theorem proving for classical logic with partial functions by reduction to Kleene logic (2017)
- Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: model representation (2016)
- Reynolds, Andrew; Blanchette, Jasmin Christian; Cruanes, Simon; Tinelli, Cesare: Model finding for recursive functions in SMT (2016)
- Bonacina, Maria Paola; Furbach, Ulrich; Sofronie-Stokkermans, Viorica: On first-order model-based reasoning (2015)
- Saghafi, Salman; Danas, Ryan; Dougherty, Daniel J.: Exploring theories with a model-finding assistant (2015)
- Hillenbrand, Thomas; Weidenbach, Christoph: Superposition for bounded domains (2013)
- Korovin, Konstantin: Inst-gen -- a modular approach to instantiation-based automated reasoning (2013)
- Lisitsa, Alexei: Finite reasons for safety (2013)
- Zhang, Hantao; Zhang, Jian: MACE4 and SEM: a comparison of finite model generators (2013)
- Baumgartner, Peter; Pelzer, Björn; Tinelli, Cesare: Model evolution with equality -- revised and implemented (2012)
- Sutcliffe, Geoff; Schulz, Stephan; Claessen, Koen; Baumgartner, Peter: The TPTP typed first-order form with arithmetic (2012)
- Déharbe, David; Fontaine, Pascal; Merz, Stephan; Woltzenlogel Paleo, Bruno: Exploiting symmetry in SMT problems (2011)
- Gebser, Martin; Sabuncu, Orkunt; Schaub, Torsten: An incremental answer set programming based system for finite model computation (2011)
- Baumgartner, Peter; Thorstensen, Evgenij: Instance based methods - A brief overview (2010) ioport
- Baumgartner, Peter; Fuchs, Alexander; de Nivelle, Hans; Tinelli, Cesare: Computing finite models by reduction to function-free clause logic (2009)
- Baumgartner, Peter; Fuchs, Alexander; Tinelli, Cesare: Lemma learning in the model evolution calculus (2006)